src/HOL/Tools/function_package/mutual.ML
changeset 30607 c3d1590debd8
parent 28965 1de908189869
child 30906 3c7a76e79898
     1.1 --- a/src/HOL/Tools/function_package/mutual.ML	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Tools/function_package/mutual.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Alexander Krauss, TU Muenchen
     1.7  
     1.8  A package for general recursive function definitions.
     1.9 @@ -207,7 +206,7 @@
    1.10                   (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
    1.11                   (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
    1.12                            THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
    1.13 -                          THEN SIMPSET' (fn ss => simp_tac (ss addsimps SumTree.proj_in_rules)) 1)
    1.14 +                          THEN (simp_tac (local_simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
    1.15          |> restore_cond 
    1.16          |> export
    1.17      end