src/Pure/envir.ML
changeset 29269 5c25a2012975
parent 26638 1d5d42d8fd66
child 30146 a77fc0209723
     1.1 --- a/src/Pure/envir.ML	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/Pure/envir.ML	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -1,7 +1,5 @@
     1.4  (*  Title:      Pure/envir.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1988  University of Cambridge
     1.8  
     1.9  Environments.  The type of a term variable / sort of a type variable is
    1.10  part of its name. The lookup function must apply type substitutions,
    1.11 @@ -118,7 +116,7 @@
    1.12  fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
    1.13        Var (nT as (name', T)) =>
    1.14          if a = name' then env     (*cycle!*)
    1.15 -        else if Term.indexname_ord (a, name') = LESS then
    1.16 +        else if TermOrd.indexname_ord (a, name') = LESS then
    1.17             (case lookup (env, nT) of  (*if already assigned, chase*)
    1.18                  NONE => update ((nT, Var (a, T)), env)
    1.19                | SOME u => vupdate ((aU, u), env))