src/Pure/context.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15801 d2f5ca3c048d
     1.1 --- a/src/Pure/context.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/context.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4  (* theory context *)
     1.5  
     1.6  local
     1.7 -  val current_theory = ref (None: theory option);
     1.8 +  val current_theory = ref (NONE: theory option);
     1.9  in
    1.10    fun get_context () = ! current_theory;
    1.11    fun set_context opt_thy = current_theory := opt_thy;
    1.12 @@ -45,19 +45,19 @@
    1.13  
    1.14  fun the_context () =
    1.15    (case get_context () of
    1.16 -    Some thy => thy
    1.17 +    SOME thy => thy
    1.18    | _ => error "Unknown theory context");
    1.19  
    1.20 -fun context thy = set_context (Some thy);
    1.21 -fun reset_context () = set_context None;
    1.22 +fun context thy = set_context (SOME thy);
    1.23 +fun reset_context () = set_context NONE;
    1.24  
    1.25  fun pass opt_thy f x =
    1.26    setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
    1.27  
    1.28  fun pass_theory thy f x =
    1.29 -  (case pass (Some thy) f x of
    1.30 -    (y, Some thy') => (y, thy')
    1.31 -  | (_, None) => error "Lost theory context in ML");
    1.32 +  (case pass (SOME thy) f x of
    1.33 +    (y, SOME thy') => (y, thy')
    1.34 +  | (_, NONE) => error "Lost theory context in ML");
    1.35  
    1.36  fun save f x = setmp (get_context ()) f x;
    1.37  
    1.38 @@ -65,7 +65,7 @@
    1.39  (* map context *)
    1.40  
    1.41  nonfix >>;
    1.42 -fun >> f = set_context (Some (f (the_context ())));
    1.43 +fun >> f = set_context (SOME (f (the_context ())));
    1.44  
    1.45  
    1.46  (* use ML text *)