discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
authorwenzelm
Tue Jul 20 23:09:49 2010 +0200 (2010-07-20)
changeset 378637f113caabcf4
parent 37862 ec81023c6861
child 37864 814b1bca7f35
discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
src/HOL/Import/proof_kernel.ML
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Typedef.thy
src/Pure/pure_setup.ML
src/Tools/Code/code_target.ML
src/Tools/Compute_Oracle/linker.ML
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Jul 20 22:03:37 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Jul 20 23:09:49 2010 +0200
     1.3 @@ -466,13 +466,11 @@
     1.4  
     1.5  fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
     1.6  
     1.7 -val check_name_thy = theory "Main"
     1.8 -
     1.9  fun valid_boundvarname s =
    1.10 -  can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) ();
    1.11 +  can (fn () => Syntax.read_term_global @{theory Main} ("SOME "^s^". True")) ();
    1.12  
    1.13  fun valid_varname s =
    1.14 -  can (fn () => Syntax.read_term_global check_name_thy s) ();
    1.15 +  can (fn () => Syntax.read_term_global @{theory Main} s) ();
    1.16  
    1.17  fun protect_varname s =
    1.18      if innocent_varname s andalso valid_varname s then s else
     2.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Tue Jul 20 22:03:37 2010 +0200
     2.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Tue Jul 20 23:09:49 2010 +0200
     2.3 @@ -82,7 +82,7 @@
     2.4  
     2.5  (*helper function in order to properly print a term*)
     2.6  
     2.7 -fun prt x = Pretty.writeln (Syntax.pretty_term_global (theory "Main") x);
     2.8 +fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x);
     2.9  
    2.10  
    2.11  (*possibility to print a given term for debugging purposes*)
    2.12 @@ -460,7 +460,7 @@
    2.13  (*mutate origTerm iter times by only exchanging subterms*)
    2.14  
    2.15  fun mutate_exc origTerm commutatives iter =
    2.16 - mutate 0 origTerm (theory "Main") commutatives [] iter;
    2.17 + mutate 0 origTerm @{theory Main} commutatives [] iter;
    2.18  
    2.19  
    2.20  (*mutate origTerm iter times by only inserting signature functions*)
     3.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Jul 20 22:03:37 2010 +0200
     3.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Jul 20 23:09:49 2010 +0200
     3.3 @@ -32,7 +32,7 @@
     3.4  (**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
     3.5  
     3.6  val collect_mem_simproc =
     3.7 -  Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     3.8 +  Simplifier.simproc @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     3.9      fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
    3.10           let val (u, _, ps) = HOLogic.strip_psplits t
    3.11           in case u of
     4.1 --- a/src/HOL/Typedef.thy	Tue Jul 20 22:03:37 2010 +0200
     4.2 +++ b/src/HOL/Typedef.thy	Tue Jul 20 23:09:49 2010 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  begin
     4.5  
     4.6  ML {*
     4.7 -structure HOL = struct val thy = theory "HOL" end;
     4.8 +structure HOL = struct val thy = @{theory HOL} end;
     4.9  *}  -- "belongs to theory HOL"
    4.10  
    4.11  locale type_definition =
     5.1 --- a/src/Pure/pure_setup.ML	Tue Jul 20 22:03:37 2010 +0200
     5.2 +++ b/src/Pure/pure_setup.ML	Tue Jul 20 23:09:49 2010 +0200
     5.3 @@ -6,8 +6,6 @@
     5.4  
     5.5  (* the Pure theories *)
     5.6  
     5.7 -val theory = Thy_Info.get_theory;
     5.8 -
     5.9  Context.>> (Context.map_theory
    5.10   (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
    5.11    Theory.end_theory));
     6.1 --- a/src/Tools/Code/code_target.ML	Tue Jul 20 22:03:37 2010 +0200
     6.2 +++ b/src/Tools/Code/code_target.ML	Tue Jul 20 23:09:49 2010 +0200
     6.3 @@ -612,7 +612,7 @@
     6.4  fun shell_command thyname cmd = Toplevel.program (fn _ =>
     6.5    (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
     6.6      ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
     6.7 -   of SOME f => (writeln "Now generating code..."; f (theory thyname))
     6.8 +   of SOME f => (writeln "Now generating code..."; f (Thy_Info.get_theory thyname))
     6.9      | NONE => error ("Bad directive " ^ quote cmd)))
    6.10    handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
    6.11  
     7.1 --- a/src/Tools/Compute_Oracle/linker.ML	Tue Jul 20 22:03:37 2010 +0200
     7.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Tue Jul 20 23:09:49 2010 +0200
     7.3 @@ -191,7 +191,7 @@
     7.4  fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
     7.5  
     7.6  local
     7.7 -    fun get_thm thmname = PureThy.get_thm (theory "Main") thmname
     7.8 +    fun get_thm thmname = PureThy.get_thm @{theory Main} thmname
     7.9      val eq_th = get_thm "HOL.eq_reflection"
    7.10  in
    7.11    fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
     8.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Tue Jul 20 22:03:37 2010 +0200
     8.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Tue Jul 20 23:09:49 2010 +0200
     8.3 @@ -207,7 +207,7 @@
     8.4  
     8.5      fun do_find () =
     8.6        let
     8.7 -        val ctxt = ProofContext.init_global (theory thy_name);
     8.8 +        val ctxt = ProofContext.init_global (Thy_Info.get_theory thy_name);
     8.9          val query = get_query ();
    8.10          val (othmslen, thms) = apsnd rev
    8.11            (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);