# HG changeset patch
# User wenzelm
# Date 1273517586 -7200
# Node ID f60e4dd6d76f982bd40a8bc155a87dd555ccefe4
# Parent  b7a62e7dec00978217d349c72cee9ec725b6262a
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;

diff -r b7a62e7dec00 -r f60e4dd6d76f src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon May 10 17:37:32 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon May 10 20:53:06 2010 +0200
@@ -92,7 +92,7 @@
 
 fun log thy s =
   let fun append_to n = if n = "" then K () else File.append (Path.explode n)
-  in append_to (Config.get_thy thy logfile) (s ^ "\n") end
+  in append_to (Config.get_global thy logfile) (s ^ "\n") end
   (* FIXME: with multithreading and parallel proofs enabled, we might need to
      encapsulate this inside a critical section *)
 
@@ -108,7 +108,7 @@
   | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
 
 fun only_within_range thy pos f x =
-  let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
+  let val l = Config.get_global thy start_line and r = Config.get_global thy end_line
   in if in_range l r (Position.line_of pos) then f x else () end
 
 in
@@ -118,7 +118,7 @@
     val thy = Proof.theory_of pre
     val pos = Toplevel.pos_of tr
     val name = Toplevel.name_of tr
-    val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
+    val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout))
 
     val str0 = string_of_int o the_default 0
     val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
diff -r b7a62e7dec00 -r f60e4dd6d76f src/Provers/blast.ML
--- a/src/Provers/blast.ML	Mon May 10 17:37:32 2010 +0200
+++ b/src/Provers/blast.ML	Mon May 10 20:53:06 2010 +0200
@@ -1278,7 +1278,7 @@
 val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
 
 fun blast_tac cs i st =
-    ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
+    ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
         (timing_depth_tac (start_timing ()) cs) 0) i
      THEN flexflex_tac) st
     handle TRANS s =>
diff -r b7a62e7dec00 -r f60e4dd6d76f src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon May 10 17:37:32 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon May 10 20:53:06 2010 +0200
@@ -355,7 +355,7 @@
   | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
 
 fun scan_config thy config =
-  let val config_type = Config.get_thy thy config
+  let val config_type = Config.get_global thy config
   in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
 
 in
diff -r b7a62e7dec00 -r f60e4dd6d76f src/Pure/config.ML
--- a/src/Pure/config.ML	Mon May 10 17:37:32 2010 +0200
+++ b/src/Pure/config.ML	Mon May 10 20:53:06 2010 +0200
@@ -16,9 +16,9 @@
   val get: Proof.context -> 'a T -> 'a
   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
   val put: 'a T -> 'a -> Proof.context -> Proof.context
-  val get_thy: theory -> 'a T -> 'a
-  val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
-  val put_thy: 'a T -> 'a -> theory -> theory
+  val get_global: theory -> 'a T -> 'a
+  val map_global: 'a T -> ('a -> 'a) -> theory -> theory
+  val put_global: 'a T -> 'a -> theory -> theory
   val get_generic: Context.generic -> 'a T -> 'a
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
@@ -83,9 +83,9 @@
 fun map_ctxt config f = Context.proof_map (map_generic config f);
 fun put_ctxt config value = map_ctxt config (K value);
 
-fun get_thy thy = get_generic (Context.Theory thy);
-fun map_thy config f = Context.theory_map (map_generic config f);
-fun put_thy config value = map_thy config (K value);
+fun get_global thy = get_generic (Context.Theory thy);
+fun map_global config f = Context.theory_map (map_generic config f);
+fun put_global config value = map_global config (K value);
 
 
 (* context information *)
diff -r b7a62e7dec00 -r f60e4dd6d76f src/Pure/unify.ML
--- a/src/Pure/unify.ML	Mon May 10 17:37:32 2010 +0200
+++ b/src/Pure/unify.ML	Mon May 10 20:53:06 2010 +0200
@@ -349,7 +349,7 @@
 fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
   : (term * (Envir.env * dpair list))Seq.seq =
 let
-  val trace_tps = Config.get_thy thy trace_types;
+  val trace_tps = Config.get_global thy trace_types;
   (*Produce copies of uarg and cons them in front of uargs*)
   fun copycons uarg (uargs, (env, dpairs)) =
   Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
@@ -584,9 +584,9 @@
 fun hounifiers (thy,env, tus : (term*term)list)
   : (Envir.env * (term*term)list)Seq.seq =
   let
-    val trace_bnd = Config.get_thy thy trace_bound;
-    val search_bnd = Config.get_thy thy search_bound;
-    val trace_smp = Config.get_thy thy trace_simp;
+    val trace_bnd = Config.get_global thy trace_bound;
+    val search_bnd = Config.get_global thy search_bound;
+    val trace_smp = Config.get_global thy trace_simp;
     fun add_unify tdepth ((env,dpairs), reseq) =
     Seq.make (fn()=>
     let val (env',flexflex,flexrigid) =