--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Mar 06 15:58:56 2015 +0100
@@ -73,10 +73,10 @@
fun prep_trm thy (x, (T, t)) =
- (Thm.cterm_of thy (Var (x, T)), Thm.cterm_of thy t)
+ (Thm.global_cterm_of thy (Var (x, T)), Thm.global_cterm_of thy t)
fun prep_ty thy (x, (S, ty)) =
- (Thm.ctyp_of thy (TVar (x, S)), Thm.ctyp_of thy ty)
+ (Thm.global_ctyp_of thy (TVar (x, S)), Thm.global_ctyp_of thy ty)
fun get_match_inst thy pat trm =
let
@@ -100,8 +100,8 @@
let
val thy = Proof_Context.theory_of ctxt
fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
- val ty_inst = map (SOME o Thm.ctyp_of thy) [domain_type (fastype_of R2)]
- val trm_inst = map (SOME o Thm.cterm_of thy) [R2, R1]
+ val ty_inst = map (SOME o Thm.global_ctyp_of thy) [domain_type (fastype_of R2)]
+ val trm_inst = map (SOME o Thm.global_cterm_of thy) [R2, R1]
in
(case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
NONE => NONE
@@ -199,10 +199,10 @@
let
val fx = fnctn x;
val thy = Proof_Context.theory_of ctxt;
- val cx = Thm.cterm_of thy x;
- val cfx = Thm.cterm_of thy fx;
- val cxt = Thm.ctyp_of thy (fastype_of x);
- val cfxt = Thm.ctyp_of thy (fastype_of fx);
+ val cx = Thm.global_cterm_of thy x;
+ val cfx = Thm.global_cterm_of thy fx;
+ val cxt = Thm.global_ctyp_of thy (fastype_of x);
+ val cfxt = Thm.global_ctyp_of thy (fastype_of fx);
val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
in
Conv.rewr_conv thm ctrm
@@ -251,8 +251,8 @@
val ty_b = fastype_of qt_arg
val ty_f = range_type (fastype_of f)
val thy = Proof_Context.theory_of context
- val ty_inst = map (SOME o Thm.ctyp_of thy) [ty_x, ty_b, ty_f]
- val t_inst = map (SOME o Thm.cterm_of thy) [R2, f, g, x, y];
+ val ty_inst = map (SOME o Thm.global_ctyp_of thy) [ty_x, ty_b, ty_f]
+ val t_inst = map (SOME o Thm.global_cterm_of thy) [R2, f, g, x, y];
val inst_thm = Drule.instantiate' ty_inst
([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
in
@@ -268,13 +268,13 @@
let
val thy = Proof_Context.theory_of ctxt
in
- case try (Thm.cterm_of thy) R of (* There can be loose bounds in R *)
+ case try (Thm.global_cterm_of thy) R of (* There can be loose bounds in R *)
SOME ctm =>
let
val ty = domain_type (fastype_of R)
in
- case try (Drule.instantiate' [SOME (Thm.ctyp_of thy ty)]
- [SOME (Thm.cterm_of thy R)]) @{thm equals_rsp} of
+ case try (Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)]
+ [SOME (Thm.global_cterm_of thy R)]) @{thm equals_rsp} of
SOME thm => rtac thm THEN' quotient_tac ctxt
| NONE => K no_tac
end
@@ -288,9 +288,9 @@
(let
val thy = Proof_Context.theory_of ctxt;
val (ty_a, ty_b) = dest_funT (fastype_of abs);
- val ty_inst = map (SOME o Thm.ctyp_of thy) [ty_a, ty_b];
+ val ty_inst = map (SOME o Thm.global_ctyp_of thy) [ty_a, ty_b];
in
- case try (map (SOME o Thm.cterm_of thy)) [rel, abs, rep] of
+ case try (map (SOME o Thm.global_cterm_of thy)) [rel, abs, rep] of
SOME t_inst =>
(case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
@@ -478,8 +478,8 @@
val thy = Proof_Context.theory_of ctxt
val (ty_b, ty_a) = dest_funT (fastype_of r1)
val (ty_c, ty_d) = dest_funT (fastype_of a2)
- val tyinst = map (SOME o Thm.ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
- val tinst = [NONE, NONE, SOME (Thm.cterm_of thy r1), NONE, SOME (Thm.cterm_of thy a2)]
+ val tyinst = map (SOME o Thm.global_ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
+ val tinst = [NONE, NONE, SOME (Thm.global_cterm_of thy r1), NONE, SOME (Thm.global_cterm_of thy a2)]
val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
@@ -488,7 +488,7 @@
then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
val thm4 =
- Drule.instantiate_normalize ([], [(Thm.cterm_of thy insp, Thm.cterm_of thy inst)]) thm3
+ Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy insp, Thm.global_cterm_of thy inst)]) thm3
in
Conv.rewr_conv thm4 ctrm
end
@@ -557,7 +557,7 @@
let
val thy = Proof_Context.theory_of ctxt
val vrs = Term.add_frees concl []
- val cvrs = map (Thm.cterm_of thy o Free) vrs
+ val cvrs = map (Thm.global_cterm_of thy o Free) vrs
val concl' = apply_under_Trueprop (all_list vrs) concl
val goal = Logic.mk_implies (concl', concl)
val rule = Goal.prove ctxt [] [] goal
@@ -617,10 +617,10 @@
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
Drule.instantiate' []
- [SOME (Thm.cterm_of thy rtrm'),
- SOME (Thm.cterm_of thy reg_goal),
+ [SOME (Thm.global_cterm_of thy rtrm'),
+ SOME (Thm.global_cterm_of thy reg_goal),
NONE,
- SOME (Thm.cterm_of thy inj_goal)] procedure_thm
+ SOME (Thm.global_cterm_of thy inj_goal)] procedure_thm
end
@@ -677,9 +677,9 @@
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
Drule.instantiate' []
- [SOME (Thm.cterm_of thy reg_goal),
+ [SOME (Thm.global_cterm_of thy reg_goal),
NONE,
- SOME (Thm.cterm_of thy inj_goal)] partiality_procedure_thm
+ SOME (Thm.global_cterm_of thy inj_goal)] partiality_procedure_thm
end