# HG changeset patch
# User wenzelm
# Date 1425682334 -3600
# Node ID a372513af1e23911afcb5e980f3caedc07afea54
# Parent  5980e75a204e53ab5519733aff687b36daedc045
clarified context;

diff -r 5980e75a204e -r a372513af1e2 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Mar 06 23:44:57 2015 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Mar 06 23:52:14 2015 +0100
@@ -153,12 +153,11 @@
 
 fun evaluation sandwich lift_postproc eval ctxt t =
   let
-    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
-    val (postproc, ct') = sandwich ctxt (cert t);
+    val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t);
   in
     Thm.term_of ct'
     |> eval ctxt
-    |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o cert)
+    |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o Thm.cterm_of ctxt)
   end;
 
 end;
@@ -168,7 +167,6 @@
 
 fun normalized_tfrees_sandwich ctxt ct =
   let
-    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
     val t = Thm.term_of ct;
     val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
@@ -179,15 +177,15 @@
   in
     if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
     then (I, ct)
-    else (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, cert (map_types normalize t))
+    else
+     (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global,
+      Thm.cterm_of ctxt (map_types normalize t))
   end;
 
 fun no_variables_sandwich ctxt ct =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.global_cterm_of thy;
-    val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
-      | t as Var _ => insert (op aconvc) (cert t)
+    val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (Thm.cterm_of ctxt t)
+      | t as Var _ => insert (op aconvc) (Thm.cterm_of ctxt t)
       | _ => I) (Thm.term_of ct) [];
     fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
       |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
diff -r 5980e75a204e -r a372513af1e2 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Mar 06 23:44:57 2015 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Mar 06 23:52:14 2015 +0100
@@ -172,12 +172,11 @@
 
 fun check_holds ctxt evaluator vs_t ct =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val t = Thm.term_of ct;
     val _ = if fastype_of t <> propT
-      then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
+      then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
       else ();
-    val iff = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
+    val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
     val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
      of SOME Holds => true
       | _ => false;
diff -r 5980e75a204e -r a372513af1e2 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Fri Mar 06 23:44:57 2015 +0100
+++ b/src/Tools/Code/code_simp.ML	Fri Mar 06 23:52:14 2015 +0100
@@ -83,7 +83,7 @@
   THEN' conclude_tac ctxt NONE ctxt;
 
 fun dynamic_value ctxt =
-  snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.global_cterm_of (Proof_Context.theory_of ctxt);
+  snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of ctxt;
 
 val _ = Theory.setup 
   (Method.setup @{binding code_simp}
diff -r 5980e75a204e -r a372513af1e2 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Mar 06 23:44:57 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Fri Mar 06 23:52:14 2015 +0100
@@ -574,7 +574,7 @@
       let
         val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
         val dom_length = length (fst (strip_type ty))
-        val thm = Axclass.unoverload_conv thy (Thm.global_cterm_of thy raw_const);
+        val thm = Axclass.unoverload_conv thy (Thm.cterm_of ctxt raw_const);
         val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in