src/ZF/Datatype.ML

   fun mk_new ([],[]) = Const("True",FOLogic.oT)
     | mk_new (largs,rargs) =
         fold_bal FOLogic.mk_conj
                  (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
 
- val datatype_ss = simpset_of (the_context ());
+ val datatype_ss = simpset ();
 
- fun proc sg _ old =
+ fun proc sg ss old =
    let val _ = if !trace then writeln ("data_free: OLD = " ^ 
                                        string_of_cterm (cterm_of sg old))
                else ()
        val (lhs,rhs) = FOLogic.dest_eq old
        val (lhead, largs) = strip_comb lhs

        val _ = if !trace then 
                  writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
                else ();
        val goal = Logic.mk_equals (old, new)
        val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
-           simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
+           simp_tac (Simplifier.inherit_bounds ss datatype_ss addsimps #free_iffs lcon_info) 1)
          handle ERROR_MESSAGE msg =>
          (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
           raise Match)
    in SOME thm end
    handle Match => NONE;
 
 
- val conv = 
-     Simplifier.simproc (Theory.sign_of (theory "ZF")) "data_free" 
-                        ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc (theory "ZF") "data_free" ["(x::i) = y"] proc;
+
 end;
 
 
 Addsimprocs [DataFree.conv];