src/ZF/Datatype.ML
changeset 12175 5cf58a1799a7
parent 12134 7049eead7a50
child 12183 c10cea75dd56
     1.1 --- a/src/ZF/Datatype.ML	Tue Nov 13 22:20:15 2001 +0100
     1.2 +++ b/src/ZF/Datatype.ML	Tue Nov 13 22:20:51 2001 +0100
     1.3 @@ -59,6 +59,7 @@
     1.4          fold_bal FOLogic.mk_conj
     1.5                   (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
     1.6  
     1.7 + val datatype_ss = simpset_of (the_context ());
     1.8  
     1.9   fun proc sg _ old =
    1.10     let val _ = if !trace then writeln ("data_free: OLD = " ^ 
    1.11 @@ -82,7 +83,7 @@
    1.12                 else ();
    1.13         val goal = Logic.mk_equals (old, new)
    1.14         val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
    1.15 -           simp_tac (simpset_of Datatype.thy addsimps #free_iffs lcon_info) 1)
    1.16 +           simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
    1.17           handle ERROR =>
    1.18           error ("data_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal)
    1.19     in Some thm end