# HG changeset patch
# User wenzelm
# Date 1425659540 -3600
# Node ID 920889b0788e03a3eb7d50dd83a6e986e77cbc5f
# Parent  deae170e24a61454d6387fd1f38eb5449d1e5092
clarified context;

diff -r deae170e24a6 -r 920889b0788e src/Pure/Isar/element.ML
--- 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
diff -r deae170e24a6 -r 920889b0788e src/Pure/Isar/expression.ML
--- 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 [];
 
diff -r deae170e24a6 -r 920889b0788e src/Pure/Isar/obtain.ML
--- 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 =
diff -r deae170e24a6 -r 920889b0788e src/Pure/Tools/rule_insts.ML
--- 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;
diff -r deae170e24a6 -r 920889b0788e src/Pure/goal.ML
--- 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;
diff -r deae170e24a6 -r 920889b0788e src/Pure/more_thm.ML
--- 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;
diff -r deae170e24a6 -r 920889b0788e src/Pure/variable.ML
--- 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;