src/Pure/unify.ML
changeset 19866 d47f32a4964a
parent 19864 227a01b8db80
child 19876 11d447d5d68c
     1.1 --- a/src/Pure/unify.ML	Mon Jun 12 21:19:05 2006 +0200
     1.2 +++ b/src/Pure/unify.ML	Mon Jun 12 21:19:06 2006 +0200
     1.3 @@ -650,11 +650,11 @@
     1.4            in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
     1.5  
     1.6          fun result env =
     1.7 -          (warning "FIXME"; if Envir.above env maxidx then
     1.8 +          if Envir.above env maxidx then
     1.9              SOME (Envir.Envir {maxidx = maxidx,
    1.10 -              iTs = Vartab.make (map (PolyML.print o (norm_tvar env)) pat_tvars),
    1.11 -              asol = Vartab.make (map (PolyML.print o (norm_var env)) pat_vars)})
    1.12 -          else NONE);
    1.13 +              iTs = Vartab.make (map (norm_tvar env) pat_tvars),
    1.14 +              asol = Vartab.make (map (norm_var env) pat_vars)})
    1.15 +          else NONE;
    1.16  
    1.17          val empty = Envir.empty maxidx';
    1.18        in