1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Aug 07 15:20:24 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Aug 07 17:01:35 2007 +0200
     1.3 @@ -231,6 +231,13 @@
     1.4                                      
     1.5              val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs 
     1.6                      orelse error (input_error "Recursive Calls not allowed in premises")
     1.7 +
     1.8 +            val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
     1.9 +            val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
    1.10 +            val _ = null funvars
    1.11 +                    orelse (warning (cat_lines ["Bound variable" ^ plural " " "s " funvars ^ commas_quote (map fst funvars) ^  
    1.12 +                                                " occur" ^ plural "s" "" funvars ^ " in function position.",  
    1.13 +                                                "Misspelled constructor???"]); true)
    1.14            in
    1.15              fqgar
    1.16            end

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