# HG changeset patch
# User wenzelm
# Date 1248383541 -7200
# Node ID e2bf2f73b0c87386f33d4c6452394d968be2fc20
# Parent  9721e8e4d48c3a9eb06648fe2eafc0bda3eef78c
more @{theory} antiquotations;

diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/FOL/simpdata.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -130,7 +130,7 @@
 
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss =
-  Simplifier.theory_context (the_context ()) empty_ss
+  Simplifier.theory_context @{theory} empty_ss
   setsubgoaler asm_simp_tac
   setSSolver (mk_solver "FOL safe" safe_solver)
   setSolver (mk_solver "FOL unsafe" unsafe_solver)
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/HOL/NSA/NSA.thy	Thu Jul 23 23:12:21 2009 +0200
@@ -684,7 +684,7 @@
 
 in
 val approx_reorient_simproc =
-  Arith_Data.prep_simproc
+  Arith_Data.prep_simproc @{theory}
     ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
 end;
 
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/HOL/Tools/arith_data.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -17,7 +17,7 @@
   val simp_all_tac: thm list -> simpset -> tactic
   val simplify_meta_eq: thm list -> simpset -> thm -> thm
   val trans_tac: thm option -> tactic
-  val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
+  val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option)
     -> simproc
 
   val setup: theory -> theory
@@ -92,7 +92,7 @@
 fun trans_tac NONE  = all_tac
   | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
 
-fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
-  Simplifier.simproc (the_context ()) name pats proc;
+fun prep_simproc thy (name, pats, proc) =
+  Simplifier.simproc thy name pats proc;
 
 end;
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -202,7 +202,7 @@
 
 
 val cancel_numerals =
-  map Arith_Data.prep_simproc
+  map (Arith_Data.prep_simproc @{theory})
    [("nateq_cancel_numerals",
      ["(l::nat) + m = n", "(l::nat) = m + n",
       "(l::nat) * m = n", "(l::nat) = m * n",
@@ -254,7 +254,8 @@
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
 
 val combine_numerals =
-  Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
+  Arith_Data.prep_simproc @{theory}
+    ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
 
 
 (*** Applying CancelNumeralFactorFun ***)
@@ -323,7 +324,7 @@
 )
 
 val cancel_numeral_factors =
-  map Arith_Data.prep_simproc
+  map (Arith_Data.prep_simproc @{theory})
    [("nateq_cancel_numeral_factors",
      ["(l::nat) * m = n", "(l::nat) = m * n"],
      K EqCancelNumeralFactor.proc),
@@ -416,7 +417,7 @@
 );
 
 val cancel_factor =
-  map Arith_Data.prep_simproc
+  map (Arith_Data.prep_simproc @{theory})
    [("nat_eq_cancel_factor",
      ["(l::nat) * m = n", "(l::nat) = m * n"],
      K EqCancelFactor.proc),
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -273,7 +273,7 @@
 );
 
 val cancel_numerals =
-  map Arith_Data.prep_simproc
+  map (Arith_Data.prep_simproc @{theory})
    [("inteq_cancel_numerals",
      ["(l::'a::number_ring) + m = n",
       "(l::'a::number_ring) = m + n",
@@ -352,13 +352,13 @@
 structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
 
 val combine_numerals =
-  Arith_Data.prep_simproc
+  Arith_Data.prep_simproc @{theory}
     ("int_combine_numerals", 
      ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
      K CombineNumerals.proc);
 
 val field_combine_numerals =
-  Arith_Data.prep_simproc
+  Arith_Data.prep_simproc @{theory}
     ("field_combine_numerals", 
      ["(i::'a::{number_ring,field,division_by_zero}) + j",
       "(i::'a::{number_ring,field,division_by_zero}) - j"], 
@@ -379,7 +379,7 @@
 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
 
 val assoc_fold_simproc =
-  Arith_Data.prep_simproc
+  Arith_Data.prep_simproc @{theory}
    ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
     K Semiring_Times_Assoc.proc);
 
@@ -453,7 +453,7 @@
 )
 
 val cancel_numeral_factors =
-  map Arith_Data.prep_simproc
+  map (Arith_Data.prep_simproc @{theory})
    [("ring_eq_cancel_numeral_factor",
      ["(l::'a::{idom,number_ring}) * m = n",
       "(l::'a::{idom,number_ring}) = m * n"],
@@ -477,7 +477,7 @@
      K DivideCancelNumeralFactor.proc)];
 
 val field_cancel_numeral_factors =
-  map Arith_Data.prep_simproc
+  map (Arith_Data.prep_simproc @{theory})
    [("field_eq_cancel_numeral_factor",
      ["(l::'a::{field,number_ring}) * m = n",
       "(l::'a::{field,number_ring}) = m * n"],
@@ -604,7 +604,7 @@
 );
 
 val cancel_factors =
-  map Arith_Data.prep_simproc
+  map (Arith_Data.prep_simproc @{theory})
    [("ring_eq_cancel_factor",
      ["(l::'a::idom) * m = n",
       "(l::'a::idom) = m * n"],
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -337,7 +337,7 @@
 		val _ = if !trace_sat then
 				tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
 			else ()
-		val False_thm = SkipProof.make_thm (the_context ()) (HOLogic.Trueprop $ HOLogic.false_const)
+		val False_thm = SkipProof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
 	in
 		(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
 		(* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
@@ -388,7 +388,7 @@
 			val msg = "SAT solver found a countermodel:\n"
 				^ (commas
 					o map (fn (term, idx) =>
-						Syntax.string_of_term_global (the_context ()) term ^ ": "
+						Syntax.string_of_term_global @{theory} term ^ ": "
 							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
 					(Termtab.dest atom_table)
 		in
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/HOL/Tools/simpdata.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -166,7 +166,7 @@
    ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
 
 val HOL_basic_ss =
-  Simplifier.theory_context (the_context ()) empty_ss
+  Simplifier.theory_context @{theory} empty_ss
     setsubgoaler asm_simp_tac
     setSSolver safe_solver
     setSolver unsafe_solver
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/HOLCF/holcf_logic.ML
--- a/src/HOLCF/holcf_logic.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/HOLCF/holcf_logic.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -34,7 +34,7 @@
 fun mk_btyp t (S,T) = Type (t,[S,T]);
 
 local
-  val intern_type = Sign.intern_type (the_context ());
+  val intern_type = Sign.intern_type @{theory};
   val u = intern_type "u";
 in
 
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/Sequents/simpdata.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -68,7 +68,7 @@
 
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss =
-  Simplifier.theory_context (the_context ()) empty_ss
+  Simplifier.theory_context @{theory} empty_ss
     setsubgoaler asm_simp_tac
     setSSolver (mk_solver "safe" safe_solver)
     setSolver (mk_solver "unsafe" unsafe_solver)
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/ZF/arith_data.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -76,8 +76,8 @@
         (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
   end;
 
-fun prep_simproc (name, pats, proc) =
-  Simplifier.simproc (the_context ()) name pats proc;
+fun prep_simproc thy (name, pats, proc) =
+  Simplifier.simproc thy name pats proc;
 
 
 (*** Use CancelNumerals simproc without binary numerals,
@@ -198,7 +198,7 @@
 
 
 val nat_cancel =
-  map prep_simproc
+  map (prep_simproc @{theory})
    [("nateq_cancel_numerals",
      ["l #+ m = n", "l = m #+ n",
       "l #* m = n", "l = m #* n",
diff -r 9721e8e4d48c -r e2bf2f73b0c8 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Thu Jul 23 22:20:37 2009 +0200
+++ b/src/ZF/int_arith.ML	Thu Jul 23 23:12:21 2009 +0200
@@ -122,8 +122,8 @@
 val int_mult_minus_simps =
     [@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2];
 
-fun prep_simproc (name, pats, proc) =
-  Simplifier.simproc (the_context ()) name pats proc;
+fun prep_simproc thy (name, pats, proc) =
+  Simplifier.simproc thy name pats proc;
 
 structure CancelNumeralsCommon =
   struct
@@ -178,7 +178,7 @@
 );
 
 val cancel_numerals =
-  map prep_simproc
+  map (prep_simproc @{theory})
    [("inteq_cancel_numerals",
      ["l $+ m = n", "l = m $+ n",
       "l $- m = n", "l = m $- n",
@@ -229,7 +229,8 @@
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
 
 val combine_numerals =
-  prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
+  prep_simproc @{theory}
+    ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
 
 
 
@@ -272,7 +273,8 @@
 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
 
 val combine_numerals_prod =
-  prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
+  prep_simproc @{theory}
+    ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
 
 end;