# HG changeset patch
# User wenzelm
# Date 1269790989 -7200
# Node ID f4f34350024925abf2672fca574066317605dbae
# Parent  992839c4be90c92fece31063d6a13b634381884d
pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;

diff -r 992839c4be90 -r f4f343500249 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Mar 28 16:59:06 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Mar 28 17:43:09 2010 +0200
@@ -36,12 +36,12 @@
   val multi_thm: thm list context_parser
   val print_configs: Proof.context -> unit
   val internal: (morphism -> attribute) -> src
-  val config_bool: bstring -> (Proof.context -> bool) -> bool Config.T * (theory -> theory)
-  val config_int: bstring -> (Proof.context -> int) -> int Config.T * (theory -> theory)
-  val config_string: bstring -> (Proof.context -> string) -> string Config.T * (theory -> theory)
-  val config_bool_global: bstring -> (Proof.context -> bool) -> bool Config.T * (theory -> theory)
-  val config_int_global: bstring -> (Proof.context -> int) -> int Config.T * (theory -> theory)
-  val config_string_global: bstring -> (Proof.context -> string) -> string Config.T * (theory -> theory)
+  val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
+  val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
+  val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
+  val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
+  val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
+  val config_string_global: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
 end;
 
 structure Attrib: ATTRIB =
diff -r 992839c4be90 -r f4f343500249 src/Pure/config.ML
--- a/src/Pure/config.ML	Sun Mar 28 16:59:06 2010 +0200
+++ b/src/Pure/config.ML	Sun Mar 28 17:43:09 2010 +0200
@@ -22,7 +22,7 @@
   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
-  val declare: bool -> string -> (Proof.context -> value) -> value T
+  val declare: bool -> string -> (Context.generic -> value) -> value T
   val name_of: 'a T -> string
 end;
 
@@ -105,7 +105,7 @@
     fun get_value context =
       (case Inttab.lookup (Value.get context) id of
         SOME value => value
-      | NONE => default (Context.proof_of context));
+      | NONE => default context);
 
     fun update_value f context =
       Value.map (Inttab.update (id, type_check name f (get_value context))) context;