# HG changeset patch
# User wenzelm
# Date 1425682355 -3600
# Node ID 4b94cc030ba08804d70187313083549f32be6edc
# Parent  a372513af1e23911afcb5e980f3caedc07afea54
clarified context;

diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_smt_normalize.ML
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Fri Mar 06 23:52:35 2015 +0100
@@ -30,7 +30,7 @@
  
 local
   val (cpfalse, cfalse) =
-    `Old_SMT_Utils.mk_cprop (Thm.global_cterm_of @{theory} @{const False})
+    `Old_SMT_Utils.mk_cprop (Thm.cterm_of @{context} @{const False})
 
   fun inst f ct thm =
     let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -203,8 +203,7 @@
     Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1
   fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct
 
-  fun mk_clist T = apply2 (Thm.global_cterm_of @{theory})
-    (HOLogic.cons_const T, HOLogic.nil_const T)
+  fun mk_clist T = apply2 (Thm.cterm_of @{context}) (HOLogic.cons_const T, HOLogic.nil_const T)
   fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   val mk_pat_list = mk_list (mk_clist @{typ pattern})
   val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"})  
diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_smt_real.ML
--- a/src/HOL/Library/Old_SMT/old_smt_real.ML	Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_real.ML	Fri Mar 06 23:52:35 2015 +0100
@@ -64,14 +64,14 @@
   fun mk_nary _ cu [] = cu
     | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
 
-  val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (real)})
-  val add = Thm.global_cterm_of @{theory} @{const plus (real)}
+  val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (real)})
+  val add = Thm.cterm_of @{context} @{const plus (real)}
   val real0 = Numeral.mk_cnumber @{ctyp real} 0
-  val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (real)})
-  val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (real)})
-  val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const divide (real)})
-  val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (real)})
-  val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (real)})
+  val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (real)})
+  val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (real)})
+  val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const divide (real)})
+  val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (real)})
+  val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (real)})
 
   fun z3_mk_builtin_fun (Old_Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
     | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("+", _)) cts =
diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_smt_solver.ML
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML	Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML	Fri Mar 06 23:52:35 2015 +0100
@@ -195,7 +195,7 @@
             const_defs = us})
         end)
 
-  val cfalse = Thm.global_cterm_of @{theory} (@{const Trueprop} $ @{const False})
+  val cfalse = Thm.cterm_of @{context} (@{const Trueprop} $ @{const False})
 in
 
 fun add_solver cfg =
@@ -268,7 +268,7 @@
 
 (* filter *)
 
-val cnot = Thm.global_cterm_of @{theory} @{const Not}
+val cnot = Thm.cterm_of @{context} @{const Not}
 
 fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
 
diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_smt_utils.ML
--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML	Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML	Fri Mar 06 23:52:35 2015 +0100
@@ -175,7 +175,7 @@
 
 val dest_all_cbinders = repeat_yield (try o dest_cbinder)
 
-val mk_cprop = Thm.apply (Thm.global_cterm_of @{theory} @{const Trueprop})
+val mk_cprop = Thm.apply (Thm.cterm_of @{context} @{const Trueprop})
 
 fun dest_cprop ct =
   (case Thm.term_of ct of
diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_z3_interface.ML
--- a/src/HOL/Library/Old_SMT/old_z3_interface.ML	Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_interface.ML	Fri Mar 06 23:52:35 2015 +0100
@@ -137,13 +137,13 @@
   | mk_builtin_num ctxt i T =
       chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
 
-val mk_true = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
-val mk_false = Thm.global_cterm_of @{theory} @{const False}
-val mk_not = Thm.apply (Thm.global_cterm_of @{theory} @{const Not})
-val mk_implies = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.implies})
-val mk_iff = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const HOL.eq (bool)})
-val conj = Thm.global_cterm_of @{theory} @{const HOL.conj}
-val disj = Thm.global_cterm_of @{theory} @{const HOL.disj}
+val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False})
+val mk_false = Thm.cterm_of @{context} @{const False}
+val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not})
+val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies})
+val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)})
+val conj = Thm.cterm_of @{context} @{const HOL.conj}
+val disj = Thm.cterm_of @{context} @{const HOL.disj}
 
 fun mk_nary _ cu [] = cu
   | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -184,15 +184,15 @@
     Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value
   end
 
-val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (int)})
-val add = Thm.global_cterm_of @{theory} @{const plus (int)}
+val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)})
+val add = Thm.cterm_of @{context} @{const plus (int)}
 val int0 = Numeral.mk_cnumber @{ctyp int} 0
-val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (int)})
-val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (int)})
-val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3div})
-val mk_mod = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const z3mod})
-val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (int)})
-val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (int)})
+val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)})
+val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)})
+val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div})
+val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod})
+val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)})
+val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)})
 
 fun mk_builtin_fun ctxt sym cts =
   (case (sym, cts) of
diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_z3_proof_literals.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML	Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML	Fri Mar 06 23:52:35 2015 +0100
@@ -82,7 +82,7 @@
       | NONE => false)
   in exists end
 
-val negate = Thm.apply (Thm.global_cterm_of @{theory} @{const Not})
+val negate = Thm.apply (Thm.cterm_of @{context} @{const Not})
 
 
 
diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_z3_proof_parser.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Fri Mar 06 23:52:35 2015 +0100
@@ -181,7 +181,7 @@
 
 (** parser context **)
 
-val not_false = Thm.global_cterm_of @{theory} (@{const Not} $ @{const False})
+val not_false = Thm.cterm_of @{context} (@{const Not} $ @{const False})
 
 fun make_context ctxt typs terms =
   let
@@ -381,7 +381,7 @@
 
 fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
 
-val ctrue = Thm.global_cterm_of @{theory} @{const True}
+val ctrue = Thm.cterm_of @{context} @{const True}
 
 fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
   (the o mk_fun (K (SOME ctrue)))) st
diff -r a372513af1e2 -r 4b94cc030ba0 src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Fri Mar 06 23:52:14 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Fri Mar 06 23:52:35 2015 +0100
@@ -229,7 +229,7 @@
             | _ => fresh_abstraction dcvs ct cx)))
   in abstr (depth, []) end
 
-val cimp = Thm.global_cterm_of @{theory} @{const Pure.imp}
+val cimp = Thm.cterm_of @{context} @{const Pure.imp}
 
 fun deepen depth f x =
   if depth = 0 then f depth x