# HG changeset patch
# User wenzelm
# Date 1425682621 -3600
# Node ID f3be9235503d85d2067aebc40841c39ab0e3759c
# Parent  929984c529d390626192c02cd3af9a656fec02dd
clarified context;

diff -r 929984c529d3 -r f3be9235503d src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Mar 06 23:57:01 2015 +0100
@@ -121,8 +121,7 @@
 local
   fun solve_cont ctxt t =
     let
-      val thy = Proof_Context.theory_of ctxt
-      val tr = instantiate' [] [SOME (Thm.global_cterm_of thy t)] @{thm Eq_TrueI}
+      val tr = instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
     in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
 in
   fun cont_proc thy =
diff -r 929984c529d3 -r f3be9235503d src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 23:57:01 2015 +0100
@@ -56,10 +56,9 @@
 
 fun remove_suc ctxt thms =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val vname = singleton (Name.variant_list (map fst
       (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
-    val cv = Thm.global_cterm_of thy (Var ((vname, 0), HOLogic.natT));
+    val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT));
     val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
     val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
     fun find_vars ct = (case Thm.term_of ct of
diff -r 929984c529d3 -r f3be9235503d src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Library/Countable.thy	Fri Mar 06 23:57:01 2015 +0100
@@ -180,8 +180,7 @@
         val alist = pred_names ~~ induct_thms
         val induct_thm = the (AList.lookup (op =) alist pred_name)
         val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
-        val thy = Proof_Context.theory_of ctxt
-        val insts = vars |> map (fn (_, T) => try (Thm.global_cterm_of thy)
+        val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
           (Const (@{const_name Countable.finite_item}, T)))
         val induct_thm' = Drule.instantiate' [] insts induct_thm
         val rules = @{thms finite_item.intros}
diff -r 929984c529d3 -r f3be9235503d src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/NSA/transfer.ML	Fri Mar 06 23:57:01 2015 +0100
@@ -52,12 +52,11 @@
 
 fun transfer_thm_of ctxt ths t =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
     val meta = Local_Defs.meta_rewrite_rule ctxt;
     val ths' = map meta ths;
     val unfolds' = map meta unfolds and refolds' = map meta refolds;
-    val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.global_cterm_of thy t))
+    val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
     val u = unstar_term consts t'
     val tac =
       rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
diff -r 929984c529d3 -r f3be9235503d src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Mar 06 23:57:01 2015 +0100
@@ -433,11 +433,11 @@
 
 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
 val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
-val ct1' = Thm.global_cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
+val ct1' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);
 
 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
 val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
-val ct2' = Thm.global_cterm_of @{theory} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
+val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
 *}
 
 end
diff -r 929984c529d3 -r f3be9235503d src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Fri Mar 06 23:57:01 2015 +0100
@@ -53,26 +53,24 @@
 val lazy_conj_simproc =
   Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
     (fn ctxt => fn t =>
-      let val thy = Proof_Context.theory_of ctxt in
-        (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
-          let
-            val P_P' = Simplifier.rewrite ctxt (Thm.global_cterm_of thy P);
-            val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2;
-          in
-            if isFalse P' then SOME (conj1_False OF [P_P'])
-            else
-              let
-                val Q_Q' = Simplifier.rewrite ctxt (Thm.global_cterm_of thy Q);
-                val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2;
-              in
-                if isFalse Q' then SOME (conj2_False OF [Q_Q'])
-                else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
-                else if P aconv P' andalso Q aconv Q' then NONE
-                else SOME (conj_cong OF [P_P', Q_Q'])
-              end
-           end
-        | _ => NONE)
-      end);
+      (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
+        let
+          val P_P' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt P);
+          val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2;
+        in
+          if isFalse P' then SOME (conj1_False OF [P_P'])
+          else
+            let
+              val Q_Q' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt Q);
+              val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2;
+            in
+              if isFalse Q' then SOME (conj2_False OF [Q_Q'])
+              else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
+              else if P aconv P' andalso Q aconv Q' then NONE
+              else SOME (conj_cong OF [P_P', Q_Q'])
+            end
+         end
+      | _ => NONE));
 
 fun string_eq_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt
@@ -113,7 +111,6 @@
       (case t of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $
                    (s as Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _)) =>
         (let
-          val thy = Proof_Context.theory_of ctxt;
           val (_::_::_::_::sT::_) = binder_types uT;
           val mi = maxidx_of_term t;
           fun mk_upds (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v $ s) =
@@ -141,7 +138,8 @@
             | mk_upds s = (Var (("s", mi + 1), sT), mi + 2);
 
           val ct =
-            Thm.global_cterm_of thy (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s));
+            Thm.cterm_of ctxt
+              (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s));
           val basic_ss = #1 (Data.get (Context.Proof ctxt));
           val ctxt' = ctxt |> Config.put simp_depth_limit 100 |> put_simpset basic_ss;
           val thm = Simplifier.rewrite ctxt' ct;
diff -r 929984c529d3 -r f3be9235503d src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Fri Mar 06 23:57:01 2015 +0100
@@ -550,7 +550,6 @@
 
 fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val (f $ arg) = Thm.term_of ct;
     val n = (case arg of @{term nat} $ n => n | n => n)
       |> HOLogic.dest_number |> snd;
@@ -560,7 +559,7 @@
         (replicate i @{term Suc});
     val _ = if arg = arg' then raise TERM ("", []) else ();
     fun propfn g = HOLogic.mk_eq (g arg, g arg')
-      |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy;
+      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
     val eq1 = Goal.prove_internal ctxt [] (propfn I)
       (K (simp_tac (put_simpset word_ss ctxt) 1));
   in Goal.prove_internal ctxt [] (propfn (curry (op $) f))
diff -r 929984c529d3 -r f3be9235503d src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Fri Mar 06 23:57:01 2015 +0100
@@ -534,7 +534,7 @@
         | and_to_list fm acc = rev (fm :: acc)
       val clauses = and_to_list prop_fm []
       val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
-      val cterms = map (Thm.global_cterm_of @{theory}) terms
+      val cterms = map (Thm.cterm_of @{context}) terms
       val start = Timing.start ()
       val _ = SAT.rawsat_thm @{context} cterms
     in
diff -r 929984c529d3 -r f3be9235503d src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy	Fri Mar 06 23:57:01 2015 +0100
@@ -111,9 +111,8 @@
 
 fun svc_tac ctxt = CSUBGOAL (fn (ct, i) =>
   let
-    val thy = Thm.theory_of_cterm ct;
     val (abs_goal, _) = svc_abstract (Thm.term_of ct);
-    val th = svc_oracle (Thm.global_cterm_of thy abs_goal);
+    val th = svc_oracle (Thm.cterm_of ctxt abs_goal);
    in compose_tac ctxt (false, th, 0) i end
    handle TERM _ => no_tac);
 *}