norm_typ -> Envir.norm_type
authorberghofe
Fri Oct 11 12:47:52 2002 +0200 (2002-10-11)
changeset 13645430310b12c5b
parent 13644 7e09ff716dc9
child 13646 46ed3d042ba5
norm_typ -> Envir.norm_type
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Thu Oct 10 19:24:34 2002 +0200
     1.2 +++ b/src/Pure/pattern.ML	Fri Oct 11 12:47:52 2002 +0200
     1.3 @@ -61,17 +61,10 @@
     1.4  fun bname binders i = fst(nth_elem(i,binders));
     1.5  fun bnames binders is = space_implode " " (map (bname binders) is);
     1.6  
     1.7 -fun norm_typ tye =
     1.8 -  let fun chase(v,s) =
     1.9 -      (case  Vartab.lookup (tye, v) of
    1.10 -        Some U => norm_typ tye U
    1.11 -      | None => TVar(v,s))
    1.12 -  in map_type_tvar chase end
    1.13 -
    1.14  fun typ_clash(tye,T,U) =
    1.15    if !trace_unify_fail
    1.16 -  then let val t = Sign.string_of_typ (!sgr) (norm_typ tye T)
    1.17 -           and u = Sign.string_of_typ (!sgr) (norm_typ tye U)
    1.18 +  then let val t = Sign.string_of_typ (!sgr) (Envir.norm_type tye T)
    1.19 +           and u = Sign.string_of_typ (!sgr) (Envir.norm_type tye U)
    1.20         in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
    1.21    else ()
    1.22