Issue a warning, when "function" encounters variables occuring in function position,
as in "f (g x) = ..." where g is a variable.

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

--- a/src/HOL/Tools/function_package/mutual.ML	Tue Aug 07 15:20:24 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Aug 07 17:01:35 2007 +0200
@@ -241,7 +241,7 @@
     in
       Goal.prove ctxt [] [] 
                  (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-                 (fn _ => SIMPSET (unfold_tac all_orig_fdefs)
+                 (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
                           THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
                           THEN SIMPSET' (fn ss => simp_tac (ss addsimps [projl_inl, projr_inr])) 1)
         |> restore_cond