src/HOL/Tools/function_package/mutual.ML
changeset 24171 25381ce95316
parent 24170 33f055a0f3a1
child 24977 9f98751c9628
--- 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