[isabelle-dev] problem with Nominal in the AFP

[Lawrence Paulson]

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")