--- a/src/Pure/Isar/element.ML Fri Mar 06 16:09:51 2015 +0100
+++ b/src/Pure/Isar/element.ML Fri Mar 06 17:32:20 2015 +0100
@@ -339,7 +339,7 @@
fun instantiate_tfrees thy subst th =
let
val idx = Thm.maxidx_of th + 1;
- fun cert_inst (a, (S, T)) = (Thm.global_ctyp_of thy (TVar ((a, idx), S)), Thm.global_ctyp_of thy T);
+ fun cert_inst (a, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, idx), S), T);
fun add_inst (a, S) insts =
if AList.defined (op =) insts a then insts
--- a/src/Pure/Isar/expression.ML Fri Mar 06 16:09:51 2015 +0100
+++ b/src/Pure/Isar/expression.ML Fri Mar 06 17:32:20 2015 +0100
@@ -630,7 +630,8 @@
in
if bodyT = propT
then (t, propT, Thm.reflexive (Thm.global_cterm_of thy t))
- else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t))
+ else
+ (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t))
end;
(* achieve plain syntax for locale predicates (without "PROP") *)
@@ -684,11 +685,11 @@
compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
compose_tac defs_ctxt
(false,
- Conjunction.intr_balanced (map (Thm.assume o Thm.global_cterm_of defs_thy) norm_ts), 0) 1);
+ Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1);
val conjuncts =
(Drule.equal_elim_rule2 OF
- [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.global_cterm_of defs_thy statement))])
+ [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_ctxt statement))])
|> Conjunction.elim_balanced (length ts);
val (_, axioms_ctxt) = defs_ctxt
@@ -705,7 +706,7 @@
fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
let
val ctxt = Proof_Context.init_global thy;
- val defs' = map (Thm.global_cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs;
+ val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs;
val (a_pred, a_intro, a_axioms, thy'') =
if null exts then (NONE, NONE, [], thy)
@@ -806,7 +807,7 @@
val notes =
if is_some asm then
[("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
- [([Assumption.assume pred_ctxt (Thm.global_cterm_of thy' (the asm))],
+ [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
[(Attrib.internal o K) Locale.witness_add])])])]
else [];
--- a/src/Pure/Isar/obtain.ML Fri Mar 06 16:09:51 2015 +0100
+++ b/src/Pure/Isar/obtain.ML Fri Mar 06 17:32:20 2015 +0100
@@ -237,20 +237,20 @@
val xs = map (apsnd norm_type o fst) vars;
val ys = map (apsnd norm_type) (drop m params);
val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
- val terms = map (Drule.mk_term o Thm.global_cterm_of thy o Free) (xs @ ys');
+ val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys');
val instT =
fold (Term.add_tvarsT o #2) params []
- |> map (TVar #> (fn T => (Thm.global_ctyp_of thy T, Thm.global_ctyp_of thy (norm_type T))));
+ |> map (TVar #> (fn T => apply2 (Thm.ctyp_of ctxt) (T, norm_type T)));
val closed_rule = rule
- |> Thm.forall_intr (Thm.global_cterm_of thy (Free thesis_var))
+ |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
|> Thm.instantiate (instT, []);
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
val vars' =
map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
(map snd vars @ replicate (length ys) NoSyn);
- val rule'' = Thm.forall_elim (Thm.global_cterm_of thy (Logic.varify_global (Free thesis_var))) rule';
+ val rule'' = Thm.forall_elim (Thm.cterm_of ctxt' (Logic.varify_global (Free thesis_var))) rule';
in ((vars', rule''), ctxt') end;
fun inferred_type (binding, _, mx) ctxt =
--- a/src/Pure/Tools/rule_insts.ML Fri Mar 06 16:09:51 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Fri Mar 06 17:32:20 2015 +0100
@@ -116,8 +116,8 @@
val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
val inst_vars = map_filter (make_inst inst2) vars2;
in
- (map (apply2 (Thm.global_ctyp_of thy)) inst_tvars,
- map (apply2 (Thm.global_cterm_of thy)) inst_vars)
+ (map (apply2 (Thm.ctyp_of ctxt)) inst_tvars,
+ map (apply2 (Thm.cterm_of ctxt)) inst_vars)
end;
fun where_rule ctxt mixed_insts fixes thm =
@@ -248,9 +248,7 @@
val envT' = map (fn (ixn, T) =>
(TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
val cenv =
- map
- (fn (xi, t) =>
- apply2 (Thm.global_cterm_of thy) (Var (xi, fastype_of t), t))
+ map (fn (xi, t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t))
(distinct
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
(xis ~~ ts));
@@ -264,7 +262,7 @@
fun liftterm t =
fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
- val lifttvar = apply2 (Thm.global_ctyp_of thy o Logic.incr_tvar inc);
+ val lifttvar = apply2 (Thm.ctyp_of ctxt' o Logic.incr_tvar inc);
val rule = Drule.instantiate_normalize
(map lifttvar envT', map liftpair cenv)
(Thm.lift_rule cgoal thm)
@@ -281,9 +279,8 @@
fun make_elim_preserve ctxt rl =
let
- val thy = Thm.theory_of_thm rl;
val maxidx = Thm.maxidx_of rl;
- fun cvar xi = Thm.global_cterm_of thy (Var (xi, propT));
+ fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT));
val revcut_rl' =
Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
(cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
--- a/src/Pure/goal.ML Fri Mar 06 16:09:51 2015 +0100
+++ b/src/Pure/goal.ML Fri Mar 06 17:32:20 2015 +0100
@@ -127,21 +127,19 @@
fun future_result ctxt result prop =
let
- val thy = Proof_Context.theory_of ctxt;
-
val assms = Assumption.all_assms_of ctxt;
val As = map Thm.term_of assms;
val xs = map Free (fold Term.add_frees (prop :: As) []);
- val fixes = map (Thm.global_cterm_of thy) xs;
+ val fixes = map (Thm.cterm_of ctxt) xs;
val tfrees = fold Term.add_tfrees (prop :: As) [];
val instT =
- map (fn (a, S) => (Thm.global_ctyp_of thy (TVar ((a, 0), S)), Thm.global_ctyp_of thy (TFree (a, S)))) tfrees;
+ map (fn (a, S) => apply2 (Thm.ctyp_of ctxt) (TVar ((a, 0), S), TFree (a, S))) tfrees;
val global_prop =
Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
- |> Thm.global_cterm_of thy
+ |> Thm.cterm_of ctxt
|> Thm.weaken_sorts (Variable.sorts_of ctxt);
val global_result = result |> Future.map
(Drule.flexflex_unique (SOME ctxt) #>
@@ -191,7 +189,7 @@
("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^
Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props)));
- fun cert_safe t = Thm.global_cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
+ fun cert_safe t = Thm.cterm_of ctxt (Envir.beta_norm (Term.no_dummy_patterns t))
handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
val casms = map cert_safe asms;
val cprops = map cert_safe props;
--- a/src/Pure/more_thm.ML Fri Mar 06 16:09:51 2015 +0100
+++ b/src/Pure/more_thm.ML Fri Mar 06 17:32:20 2015 +0100
@@ -118,7 +118,9 @@
let
val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
- in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.global_cterm_of thy v) | _ => I) t end;
+ in
+ Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.global_cterm_of thy v) | _ => I) t
+ end;
(* cterm constructors and destructors *)
@@ -349,8 +351,8 @@
(* certify_instantiate *)
fun certify_inst thy (instT, inst) =
- (map (fn (v, T) => (Thm.global_ctyp_of thy (TVar v), Thm.global_ctyp_of thy T)) instT,
- map (fn (v, t) => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy t)) inst);
+ (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT,
+ map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst);
fun certify_instantiate insts th =
Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
--- a/src/Pure/variable.ML Fri Mar 06 16:09:51 2015 +0100
+++ b/src/Pure/variable.ML Fri Mar 06 17:32:20 2015 +0100
@@ -587,9 +587,8 @@
fun focus_cterm goal ctxt =
let
- val thy = Thm.theory_of_cterm goal;
val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
- val ps' = map (Thm.global_cterm_of thy o Free) ps;
+ val ps' = map (Thm.cterm_of ctxt' o Free) ps;
val goal' = fold forall_elim_prop ps' goal;
in ((xs ~~ ps', goal'), ctxt') end;