src/Pure/type_infer.ML
changeset 15531 08c8dad8e399
parent 14993 802f3732a54e
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/type_infer.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/type_infer.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -120,8 +120,8 @@
     1.4  
     1.5      fun pre_of (TVar (v as (xi, _))) =
     1.6            (case assoc (params', xi) of
     1.7 -            None => PTVar v
     1.8 -          | Some p => p)
     1.9 +            NONE => PTVar v
    1.10 +          | SOME p => p)
    1.11        | pre_of (TFree ("'_dummy_", S)) = mk_param S
    1.12        | pre_of (TFree v) = PTFree v
    1.13        | pre_of (T as Type (a, Ts)) =
    1.14 @@ -162,8 +162,8 @@
    1.15  
    1.16      fun pre_of (ps, Const (c, T)) =
    1.17            (case const_type c of
    1.18 -            Some U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T
    1.19 -          | None => raise TYPE ("No such constant: " ^ quote c, [], []))
    1.20 +            SOME U => constrain (ps, PConst (c, snd (pretyp_of (K true) ([], U)))) T
    1.21 +          | NONE => raise TYPE ("No such constant: " ^ quote c, [], []))
    1.22        | pre_of (ps, Var (xi, Type ("_polymorphic_", [T]))) =
    1.23            (ps, PVar (xi, snd (pretyp_of (K true) ([], T))))
    1.24        | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
    1.25 @@ -408,8 +408,8 @@
    1.26      val _ = seq (fn t => (infer pp classes arities t; ())) tTs';
    1.27  
    1.28      (*collect result unifier*)
    1.29 -    fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); None)
    1.30 -      | ch_var xi_T = Some xi_T;
    1.31 +    fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE)
    1.32 +      | ch_var xi_T = SOME xi_T;
    1.33      val env = mapfilter ch_var Tps;
    1.34  
    1.35      (*convert back to terms/typs*)
    1.36 @@ -458,10 +458,10 @@
    1.37  
    1.38      fun get xi =
    1.39        (case (assoc (env, xi), def_sort xi) of
    1.40 -        (None, None) => Type.defaultS tsig
    1.41 -      | (None, Some S) => S
    1.42 -      | (Some S, None) => S
    1.43 -      | (Some S, Some S') =>
    1.44 +        (NONE, NONE) => Type.defaultS tsig
    1.45 +      | (NONE, SOME S) => S
    1.46 +      | (SOME S, NONE) => S
    1.47 +      | (SOME S, SOME S') =>
    1.48            if Type.eq_sort tsig (S, S') then S'
    1.49            else error ("Sort constraint inconsistent with default for type variable " ^
    1.50              quote (Syntax.string_of_vname' xi)));