src/Pure/envir.ML
changeset 15531 08c8dad8e399
parent 12496 0a9bd5034e05
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/envir.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/envir.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -74,10 +74,10 @@
     1.4  (*Determine if the least index updated exceeds lim*)
     1.5  fun above (lim, Envir {asol, iTs, ...}) =
     1.6    (case (Vartab.min_key asol, Vartab.min_key iTs) of
     1.7 -     (None, None) => true
     1.8 -   | (Some (_, i), None) => i > lim
     1.9 -   | (None, Some (_, i')) => i' > lim
    1.10 -   | (Some (_, i), Some (_, i')) => i > lim andalso i' > lim);
    1.11 +     (NONE, NONE) => true
    1.12 +   | (SOME (_, i), NONE) => i > lim
    1.13 +   | (NONE, SOME (_, i')) => i' > lim
    1.14 +   | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
    1.15  
    1.16  (*Update, checking Var-Var assignments: try to suppress higher indexes*)
    1.17  fun vupdate((a,t), env) = case t of
    1.18 @@ -85,8 +85,8 @@
    1.19          if a=name' then env     (*cycle!*)
    1.20          else if xless(a, name')  then
    1.21             (case lookup(env,name') of  (*if already assigned, chase*)
    1.22 -                None => update((name', Var(a,T)), env)
    1.23 -              | Some u => vupdate((a,u), env))
    1.24 +                NONE => update((name', Var(a,T)), env)
    1.25 +              | SOME u => vupdate((a,u), env))
    1.26          else update((a,t), env)
    1.27      | _ => update((a,t), env);
    1.28  
    1.29 @@ -105,8 +105,8 @@
    1.30  fun norm_term1 same (asol,t) : term =
    1.31    let fun norm (Var (w,T)) =
    1.32              (case Vartab.lookup (asol, w) of
    1.33 -                Some u => (norm u handle SAME => u)
    1.34 -              | None   => raise SAME)
    1.35 +                SOME u => (norm u handle SAME => u)
    1.36 +              | NONE   => raise SAME)
    1.37          | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
    1.38          | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
    1.39          | norm (f $ t) =
    1.40 @@ -121,8 +121,8 @@
    1.41  fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
    1.42    | normT iTs (TFree _) = raise SAME
    1.43    | normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
    1.44 -          Some U => normTh iTs U
    1.45 -        | None => raise SAME)
    1.46 +          SOME U => normTh iTs U
    1.47 +        | NONE => raise SAME)
    1.48  and normTh iTs T = ((normT iTs T) handle SAME => T)
    1.49  and normTs iTs [] = raise SAME
    1.50    | normTs iTs (T :: Ts) =
    1.51 @@ -134,8 +134,8 @@
    1.52          | norm (Free (a, T)) = Free(a, normT iTs T)
    1.53          | norm (Var (w, T)) =
    1.54              (case Vartab.lookup (asol, w) of
    1.55 -                Some u => normh u
    1.56 -              | None   => Var(w, normT iTs T))
    1.57 +                SOME u => normh u
    1.58 +              | NONE   => Var(w, normT iTs T))
    1.59          | norm (Abs (a, T, body)) =
    1.60                 (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
    1.61          | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
    1.62 @@ -170,8 +170,8 @@
    1.63  fun head_norm env t =
    1.64    let
    1.65      fun hnorm (Var (v, T)) = (case lookup (env, v) of
    1.66 -          Some u => head_norm env u
    1.67 -        | None => raise SAME)
    1.68 +          SOME u => head_norm env u
    1.69 +        | NONE => raise SAME)
    1.70        | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
    1.71        | hnorm (Abs (_, _, body) $ t) =
    1.72            head_norm env (subst_bound (t, body))
    1.73 @@ -191,7 +191,7 @@
    1.74  	   Type ("fun", [_, T]) => T
    1.75  	 | TVar(ixn, _) =>
    1.76  		(case Vartab.lookup (iTs, ixn) of
    1.77 -		   Some (Type ("fun", [_, T])) => T
    1.78 +		   SOME (Type ("fun", [_, T])) => T
    1.79  		 | _ => raise TERM (funerr, [f $ u]))
    1.80  	 | _ => raise TERM (funerr, [f $ u]))
    1.81        | fast Ts (Const (_, T)) = T