# HG changeset patch
# User wenzelm
# Date 1279660189 -7200
# Node ID 7f113caabcf441594b54642ee25283b9f697b8be
# Parent  ec81023c68615982461e098fcbc785427893a4a7
discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;

diff -r ec81023c6861 -r 7f113caabcf4 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Tue Jul 20 22:03:37 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Tue Jul 20 23:09:49 2010 +0200
@@ -466,13 +466,11 @@
 
 fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
 
-val check_name_thy = theory "Main"
-
 fun valid_boundvarname s =
-  can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) ();
+  can (fn () => Syntax.read_term_global @{theory Main} ("SOME "^s^". True")) ();
 
 fun valid_varname s =
-  can (fn () => Syntax.read_term_global check_name_thy s) ();
+  can (fn () => Syntax.read_term_global @{theory Main} s) ();
 
 fun protect_varname s =
     if innocent_varname s andalso valid_varname s then s else
diff -r ec81023c6861 -r 7f113caabcf4 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Tue Jul 20 22:03:37 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Tue Jul 20 23:09:49 2010 +0200
@@ -82,7 +82,7 @@
 
 (*helper function in order to properly print a term*)
 
-fun prt x = Pretty.writeln (Syntax.pretty_term_global (theory "Main") x);
+fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x);
 
 
 (*possibility to print a given term for debugging purposes*)
@@ -460,7 +460,7 @@
 (*mutate origTerm iter times by only exchanging subterms*)
 
 fun mutate_exc origTerm commutatives iter =
- mutate 0 origTerm (theory "Main") commutatives [] iter;
+ mutate 0 origTerm @{theory Main} commutatives [] iter;
 
 
 (*mutate origTerm iter times by only inserting signature functions*)
diff -r ec81023c6861 -r 7f113caabcf4 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Jul 20 22:03:37 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Tue Jul 20 23:09:49 2010 +0200
@@ -32,7 +32,7 @@
 (**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
 
 val collect_mem_simproc =
-  Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
+  Simplifier.simproc @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
          let val (u, _, ps) = HOLogic.strip_psplits t
          in case u of
diff -r ec81023c6861 -r 7f113caabcf4 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Tue Jul 20 22:03:37 2010 +0200
+++ b/src/HOL/Typedef.thy	Tue Jul 20 23:09:49 2010 +0200
@@ -13,7 +13,7 @@
 begin
 
 ML {*
-structure HOL = struct val thy = theory "HOL" end;
+structure HOL = struct val thy = @{theory HOL} end;
 *}  -- "belongs to theory HOL"
 
 locale type_definition =
diff -r ec81023c6861 -r 7f113caabcf4 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Jul 20 22:03:37 2010 +0200
+++ b/src/Pure/pure_setup.ML	Tue Jul 20 23:09:49 2010 +0200
@@ -6,8 +6,6 @@
 
 (* the Pure theories *)
 
-val theory = Thy_Info.get_theory;
-
 Context.>> (Context.map_theory
  (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
   Theory.end_theory));
diff -r ec81023c6861 -r 7f113caabcf4 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Jul 20 22:03:37 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Jul 20 23:09:49 2010 +0200
@@ -612,7 +612,7 @@
 fun shell_command thyname cmd = Toplevel.program (fn _ =>
   (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
     ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
-   of SOME f => (writeln "Now generating code..."; f (theory thyname))
+   of SOME f => (writeln "Now generating code..."; f (Thy_Info.get_theory thyname))
     | NONE => error ("Bad directive " ^ quote cmd)))
   handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 
diff -r ec81023c6861 -r 7f113caabcf4 src/Tools/Compute_Oracle/linker.ML
--- a/src/Tools/Compute_Oracle/linker.ML	Tue Jul 20 22:03:37 2010 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML	Tue Jul 20 23:09:49 2010 +0200
@@ -191,7 +191,7 @@
 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
 
 local
-    fun get_thm thmname = PureThy.get_thm (theory "Main") thmname
+    fun get_thm thmname = PureThy.get_thm @{theory Main} thmname
     val eq_th = get_thm "HOL.eq_reflection"
 in
   fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
diff -r ec81023c6861 -r 7f113caabcf4 src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Tue Jul 20 22:03:37 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Tue Jul 20 23:09:49 2010 +0200
@@ -207,7 +207,7 @@
 
     fun do_find () =
       let
-        val ctxt = ProofContext.init_global (theory thy_name);
+        val ctxt = ProofContext.init_global (Thy_Info.get_theory thy_name);
         val query = get_query ();
         val (othmslen, thms) = apsnd rev
           (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);