src/Pure/term.ML
changeset 15531 08c8dad8e399
parent 15472 4674102737e9
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/term.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/term.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -468,7 +468,7 @@
     1.4            Abs (if_none (assoc_string (ren, x)) x, T, ren_abs b)
     1.5        | ren_abs (f $ t) = ren_abs f $ ren_abs t
     1.6        | ren_abs t = t
     1.7 -  in if null ren then None else Some (ren_abs t) end;
     1.8 +  in if null ren then NONE else SOME (ren_abs t) end;
     1.9  
    1.10  (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
    1.11     (Bound 0) is loose at level 0 *)
    1.12 @@ -596,8 +596,8 @@
    1.13    | subst_free pairs =
    1.14        let fun substf u =
    1.15              case gen_assoc (op aconv) (pairs, u) of
    1.16 -                Some u' => u'
    1.17 -              | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
    1.18 +                SOME u' => u'
    1.19 +              | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
    1.20                                   | t$u' => substf t $ substf u'
    1.21                                   | _ => u)
    1.22        in  substf  end;
    1.23 @@ -671,8 +671,8 @@
    1.24    let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
    1.25          | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)
    1.26          | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of
    1.27 -            None   => Var(ixn,typ_subst_TVars iTs T)
    1.28 -          | Some t => t)
    1.29 +            NONE   => Var(ixn,typ_subst_TVars iTs T)
    1.30 +          | SOME t => t)
    1.31          | subst(b as Bound _) = b
    1.32          | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)
    1.33          | subst(f$t) = subst f $ subst t
    1.34 @@ -1011,7 +1011,7 @@
    1.35    let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
    1.36          | subst(T as TFree _) = T
    1.37          | subst(T as TVar(ixn, _)) =
    1.38 -            (case Vartab.lookup (iTs, ixn) of None => T | Some(U) => U)
    1.39 +            (case Vartab.lookup (iTs, ixn) of NONE => T | SOME(U) => U)
    1.40    in subst T end;
    1.41  
    1.42  (*Substitute for type Vars in a term, version using Vartab*)
    1.43 @@ -1029,8 +1029,8 @@
    1.44  
    1.45  fun compress_type T =
    1.46    (case Typtab.lookup (! memo_types, T) of
    1.47 -    Some T' => T'
    1.48 -  | None =>
    1.49 +    SOME T' => T'
    1.50 +  | NONE =>
    1.51        let val T' = (case T of Type (a, Ts) => Type (a, map compress_type Ts) | _ => T)
    1.52        in memo_types := Typtab.update ((T', T'), ! memo_types); T' end);
    1.53  
    1.54 @@ -1043,8 +1043,8 @@
    1.55    | share_term (Abs (a, T, u)) = Abs (a, T, share_term u)
    1.56    | share_term t =
    1.57        (case Termtab.lookup (! memo_terms, t) of
    1.58 -        Some t' => t'
    1.59 -      | None => (memo_terms := Termtab.update ((t, t), ! memo_terms); t));
    1.60 +        SOME t' => t'
    1.61 +      | NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t));
    1.62  
    1.63  val compress_term = share_term o map_term_types compress_type;
    1.64