src/Pure/unify.ML
changeset 19876 11d447d5d68c
parent 19866 d47f32a4964a
child 19920 8257e52164a1
     1.1 --- a/src/Pure/unify.ML	Tue Jun 13 23:41:37 2006 +0200
     1.2 +++ b/src/Pure/unify.ML	Tue Jun 13 23:41:39 2006 +0200
     1.3 @@ -31,8 +31,7 @@
     1.4  val trace_bound = ref 25  (*tracing starts above this depth, 0 for full*)
     1.5  and search_bound = ref 30 (*unification quits above this depth*)
     1.6  and trace_simp = ref false  (*print dpairs before calling SIMPL*)
     1.7 -and trace_types = ref false (*announce potential incompleteness
     1.8 -          of type unification*)
     1.9 +and trace_types = ref false (*announce potential incompleteness of type unification*)
    1.10  
    1.11  type binderlist = (string*typ) list;
    1.12  
    1.13 @@ -650,7 +649,7 @@
    1.14            in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
    1.15  
    1.16          fun result env =
    1.17 -          if Envir.above env maxidx then
    1.18 +          if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
    1.19              SOME (Envir.Envir {maxidx = maxidx,
    1.20                iTs = Vartab.make (map (norm_tvar env) pat_tvars),
    1.21                asol = Vartab.make (map (norm_var env) pat_vars)})
    1.22 @@ -658,7 +657,8 @@
    1.23  
    1.24          val empty = Envir.empty maxidx';
    1.25        in
    1.26 -        Seq.append (pattern_matchers thy pairs empty)
    1.27 +        Seq.append
    1.28 +          (pattern_matchers thy pairs empty)
    1.29            (Seq.map_filter result (smash_unifiers thy pairs' empty))
    1.30        end;
    1.31