--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Mar 06 15:58:56 2015 +0100
@@ -46,7 +46,7 @@
Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
Var (("P", 0), HOLogic.boolT));
val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
- val insts' = map (Thm.cterm_of thy) induct_Ps ~~ map (Thm.cterm_of thy) insts;
+ val insts' = map (Thm.global_cterm_of thy) induct_Ps ~~ map (Thm.global_cterm_of thy) insts;
val induct' =
refl RS
(nth (Old_Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i
@@ -208,7 +208,7 @@
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
val induct' = induct
|> cterm_instantiate
- (map (Thm.cterm_of thy1) induct_Ps ~~ map (Thm.cterm_of thy1) insts);
+ (map (Thm.global_cterm_of thy1) induct_Ps ~~ map (Thm.global_cterm_of thy1) insts);
in
Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
(HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
@@ -381,7 +381,7 @@
let
val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
val exhaustion' = exhaustion
- |> cterm_instantiate [apply2 (Thm.cterm_of thy) (lhs, Free ("x", T))];
+ |> cterm_instantiate [apply2 (Thm.global_cterm_of thy) (lhs, Free ("x", T))];
fun tac ctxt =
EVERY [resolve_tac ctxt [exhaustion'] 1,
ALLGOALS (asm_simp_tac
@@ -453,7 +453,7 @@
val nchotomy' = nchotomy RS spec;
val [v] = Term.add_vars (Thm.concl_of nchotomy') [];
val nchotomy'' =
- cterm_instantiate [apply2 (Thm.cterm_of thy) (Var v, Ma)] nchotomy';
+ cterm_instantiate [apply2 (Thm.global_cterm_of thy) (Var v, Ma)] nchotomy';
in
Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {context = ctxt, prems, ...} =>