Incompleteness FAILED
(see also
/media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.6_x86_64-linux/log/Incompleteness)
*** Specification.definition NONE [] ((permute_def_name, []), permute_eqn)
*** : Attrib.binding * term ->
*** local_theory -> (term * (string * thm)) * local_theory
*** Argument: lthy : local_theory
*** Reason:
*** Can't unify local_theory to Attrib.binding * term (Incompatible types)
*** ML error (line 60 of "~~/afp/thys/Nominal2/nominal_atoms.ML"):
*** Pattern and expression have incompatible types.
*** Pattern: ((_, (_, permute_ldef)), lthy) : ('a * ('b * 'c)) * 'd
*** Expression:
*** Specification.definition NONE []
*** ((permute_def_name, [...]), permute_eqn)
*** lthy
*** : local_theory -> (term * (string * thm)) * local_theory
*** Reason:
*** Can't unify ('a * ('b * 'c)) * 'd to
*** local_theory -> (term * (string * thm)) * local_theory
*** (Incompatible types)
*** ML error (line 63 of "~~/afp/thys/Nominal2/nominal_atoms.ML"):
*** Type error in function application.
*** Function: Specification.definition NONE [] :
*** term list ->
*** Attrib.binding * term ->
*** local_theory -> (term * (string * thm)) * local_theory
*** Argument: ((atom_def_name, []), atom_eqn) : (binding * 'a list) * term
*** Reason:
*** Can't unify term list to (binding * 'a list) * term
*** (Incompatible types)
*** ML error (line 62 of "~~/afp/thys/Nominal2/nominal_atoms.ML"):
*** Pattern and expression have incompatible types.
*** Pattern: ((_, (_, atom_ldef)), lthy) : ('a * ('b * 'c)) * 'd
*** Expression:
*** Specification.definition NONE [] ((atom_def_name, [...]), atom_eqn)
*** lthy
*** : local_theory -> (term * (string * thm)) * local_theory
*** Reason:
*** Can't unify ('a * ('b * 'c)) * 'd to
*** local_theory -> (term * (string * thm)) * local_theory
*** (Incompatible types)
*** At command "ML_file" (line 3433 of "~~/afp/thys/Nominal2/Nominal2_Base.thy")
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
