src/Pure/config.ML
changeset 36002 f4f343500249
parent 36000 5560b2437789
child 36787 f60e4dd6d76f
     1.1 --- a/src/Pure/config.ML	Sun Mar 28 16:59:06 2010 +0200
     1.2 +++ b/src/Pure/config.ML	Sun Mar 28 17:43:09 2010 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    val get_generic: Context.generic -> 'a T -> 'a
     1.5    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
     1.6    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
     1.7 -  val declare: bool -> string -> (Proof.context -> value) -> value T
     1.8 +  val declare: bool -> string -> (Context.generic -> value) -> value T
     1.9    val name_of: 'a T -> string
    1.10  end;
    1.11  
    1.12 @@ -105,7 +105,7 @@
    1.13      fun get_value context =
    1.14        (case Inttab.lookup (Value.get context) id of
    1.15          SOME value => value
    1.16 -      | NONE => default (Context.proof_of context));
    1.17 +      | NONE => default context);
    1.18  
    1.19      fun update_value f context =
    1.20        Value.map (Inttab.update (id, type_check name f (get_value context))) context;