diff -r 6f43714517ee -r 08c8dad8e399 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Pure/type_infer.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -120,8 +120,8 @@
 
     fun pre_of (TVar (v as (xi, _))) =
           (case assoc (params', xi) of
-            None => PTVar v
-          | Some p => p)
+            NONE => PTVar v
+          | SOME p => p)
       | pre_of (TFree ("'_dummy_", S)) = mk_param S
       | pre_of (TFree v) = PTFree v
       | pre_of (T as Type (a, Ts)) =
@@ -162,8 +162,8 @@
 
     fun pre_of (ps, Const (c, T)) =
           (case const_type c of
-            Some U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T
-          | None => raise TYPE ("No such constant: " ^ quote c, [], []))
+            SOME U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T
+          | NONE => raise TYPE ("No such constant: " ^ quote c, [], []))
       | pre_of (ps, Var (xi, Type ("_polymorphic_", [T]))) =
           (ps, PVar (xi, snd (pretyp_of (K true) ([], T))))
       | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
@@ -408,8 +408,8 @@
     val _ = seq (fn t => (infer pp classes arities t; ())) tTs';
 
     (*collect result unifier*)
-    fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); None)
-      | ch_var xi_T = Some xi_T;
+    fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE)
+      | ch_var xi_T = SOME xi_T;
     val env = mapfilter ch_var Tps;
 
     (*convert back to terms/typs*)
@@ -458,10 +458,10 @@
 
     fun get xi =
       (case (assoc (env, xi), def_sort xi) of
-        (None, None) => Type.defaultS tsig
-      | (None, Some S) => S
-      | (Some S, None) => S
-      | (Some S, Some S') =>
+        (NONE, NONE) => Type.defaultS tsig
+      | (NONE, SOME S) => S
+      | (SOME S, NONE) => S
+      | (SOME S, SOME S') =>
           if Type.eq_sort tsig (S, S') then S'
           else error ("Sort constraint inconsistent with default for type variable " ^
             quote (Syntax.string_of_vname' xi)));