diff -r 3b8232f56941 -r 9f44608ea28d Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Thu Mar 31 15:25:35 2011 +0200
+++ b/Nominal/nominal_function.ML	Wed Apr 06 13:47:08 2011 +0100
@@ -40,6 +40,68 @@
 open Function_Lib
 open Function_Common
 
+
+
+(* Check for all sorts of errors in the input - nominal needs a different checking function *)
+fun nominal_check_defs ctxt fixes eqs =
+  let
+    val fnames = map (fst o fst) fixes
+
+    fun check geq =
+      let
+        fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
+
+        fun check_head fname =
+          member (op =) fnames fname orelse
+          input_error ("Illegal equation head. Expected " ^ commas_quote fnames)
+
+        val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq
+
+        val _ = length args > 0 orelse input_error "Function has no arguments:"
+
+        fun add_bvs t is = add_loose_bnos (t, 0, is)
+        val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
+                    |> map (fst o nth (rev qs))
+
+        val _ = forall (not o Term.exists_subterm
+          (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args)
+          orelse input_error "Defined function may not occur in premises or arguments"
+
+        val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
+        val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
+        val _ = null funvars orelse (warning (cat_lines
+          ["Bound variable" ^ plural " " "s " funvars ^
+          commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
+          " in function position.", "Misspelled constructor???"]); true)
+      in
+        (fname, length args)
+      end
+
+    val grouped_args = AList.group (op =) (map check eqs)
+    val _ = grouped_args
+      |> map (fn (fname, ars) =>
+        length (distinct (op =) ars) = 1
+        orelse error ("Function " ^ quote fname ^
+          " has different numbers of arguments in different equations"))
+
+    val not_defined = subtract (op =) (map fst grouped_args) fnames
+    val _ = null not_defined
+      orelse error ("No defining equations for function" ^
+        plural " " "s " not_defined ^ commas_quote not_defined)
+
+    fun check_sorts ((fname, fT), _) =
+      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
+      orelse error (cat_lines
+      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
+       Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
+
+    val _ = map check_sorts fixes
+  in
+    ()
+  end
+
+
+
 val simp_attribs = map (Attrib.internal o K)
   [Simplifier.simp_add,
    Code.add_default_eqn_attribute,
@@ -78,7 +140,7 @@
     val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
     val fixes = map (apfst (apfst Binding.name_of)) fixes0;
     val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
-    val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
+    val (eqs, post, sort_cont, cnames) =  empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
 
     val defname = mk_defname fixes
     val FunctionConfig {partials, default, ...} = config
@@ -175,6 +237,7 @@
 val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
 
 
+
 (* setup *)
 
 val setup =