--- 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;
--- 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;