# HG changeset patch
# User wenzelm
# Date 1436116372 -7200
# Node ID 54bc3517161e69baef97f1ddd9fa0f1a79d87f8a
# Parent  441e268564c7ec6ed3a7ad042f86c9f4617eefed
clarified context;

diff -r 441e268564c7 -r 54bc3517161e src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sun Jul 05 19:08:40 2015 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sun Jul 05 19:12:52 2015 +0200
@@ -17,7 +17,7 @@
     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
@@ -343,10 +343,9 @@
 
   (*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