src/HOL/Tools/function_package/fundef_common.ML
changeset 24171 25381ce95316
parent 24170 33f055a0f3a1
child 24920 2a45e400fdad
--- 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