# HG changeset patch
# User wenzelm
# Date 1425672867 -3600
# Node ID a6e977d8b0709413a23cd9761adf51642ce398d7
# Parent  aacdce52b2fce4f0b110a3b4a2c49c41026db377
clarified context;

diff -r aacdce52b2fc -r a6e977d8b070 src/ZF/Tools/cartprod.ML
--- a/src/ZF/Tools/cartprod.ML	Fri Mar 06 20:08:45 2015 +0100
+++ b/src/ZF/Tools/cartprod.ML	Fri Mar 06 21:14:27 2015 +0100
@@ -106,10 +106,10 @@
 fun split_rule_var ctxt (Var(v,_), Type("fun",[T1,T2]), rl) =
       let val T' = factors T1 ---> T2
           val newt = ap_split T1 T2 (Var(v,T'))
-          val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl)
       in
-          remove_split ctxt (Drule.instantiate_normalize ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
-                                           cterm newt)]) rl)
+        remove_split ctxt
+          (Drule.instantiate_normalize ([],
+            [apply2 (Thm.cterm_of ctxt) (Var(v, Ind_Syntax.iT-->T2), newt)]) rl)
       end
   | split_rule_var _ (t,T,rl) = rl;
 
diff -r aacdce52b2fc -r a6e977d8b070 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Fri Mar 06 20:08:45 2015 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Mar 06 21:14:27 2015 +0100
@@ -30,6 +30,7 @@
 fun smart_cases ctxt s =
   let
     val thy = Proof_Context.theory_of ctxt;
+
     fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
     val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
     val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
@@ -37,7 +38,7 @@
   in
     (case Symtab.lookup (IndCasesData.get thy) c of
       NONE => error ("Unknown inductive cases rule for set " ^ quote c)
-    | SOME f => f ctxt (Thm.global_cterm_of thy A))
+    | SOME f => f ctxt (Thm.cterm_of ctxt A))
   end;