--- a/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 23:56:43 2015 +0100
@@ -105,11 +105,11 @@
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
- val inst = map (apply2 (Thm.global_cterm_of thy)) (map head_of (HOLogic.dest_conj
+ val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
val thm =
- Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems) (Thm.global_cterm_of thy concl)
+ Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
(fn prems =>
EVERY [
rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
@@ -185,12 +185,12 @@
val y' = Free ("y", T);
val thm =
- Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems)
- (Thm.global_cterm_of thy
+ Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems)
+ (Thm.cterm_of ctxt
(HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
(fn prems =>
EVERY [
- rtac (cterm_instantiate [apply2 (Thm.global_cterm_of thy) (y, y')] exhaust) 1,
+ rtac (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust) 1,
ALLGOALS (EVERY'
[asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])