--- a/src/HOL/Tools/function_package/fundef_common.ML Tue Aug 07 15:20:24 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Aug 07 17:01:35 2007 +0200
@@ -231,6 +231,13 @@
val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs
orelse error (input_error "Recursive Calls not allowed in premises")
+
+ 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
fqgar
end