src/ZF/Tools/datatype_package.ML

    {con_defs   : thm list,             (*definitions made in thy*)
     case_eqns  : thm list,             (*equations for case operator*)
     recursor_eqns : thm list,          (*equations for the recursor*)
     free_iffs  : thm list,             (*freeness rewrite rules*)
     free_SEs   : thm list,             (*freeness destruct rules*)
-    mk_free    : string -> thm};       (*function to make freeness theorems*)
+    mk_free    : Proof.context -> string -> thm};    (*function to make freeness theorems*)
 
 signature DATATYPE_ARG =
 sig
   val intrs : thm list
   val elims : thm list

 
   val {intrs, elim, induct, mutual_induct, ...} = ind_result
 
   (*Typical theorems have the form ~con1=con2, con1=con2==>False,
     con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
-  fun mk_free s =
+  fun mk_free ctxt s =
     let
-      val thy = Thm.theory_of_thm elim;
-      val ctxt = Proof_Context.init_global thy;
+      val thy = Proof_Context.theory_of ctxt;
     in
       Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
         (fn {context = ctxt', ...} => EVERY
          [rewrite_goals_tac ctxt' con_defs,
           fast_tac (put_claset ZF_cs ctxt' addSEs free_SEs @ Su.free_SEs) 1])