1.1 --- a/src/Tools/eqsubst.ML	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -235,13 +235,13 @@
     1.4            val initenv =
     1.5              Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
     1.6            val useq = Unify.smash_unifiers thry [a] initenv
     1.7 -	            handle UnequalLengths => Seq.empty
     1.8 -		               | Term.TERM _ => Seq.empty;
     1.9 +              handle UnequalLengths => Seq.empty
    1.10 +                   | Term.TERM _ => Seq.empty;
    1.11            fun clean_unify' useq () =
    1.12                (case (Seq.pull useq) of
    1.13                   NONE => NONE
    1.14                 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
    1.15 -	            handle UnequalLengths => NONE
    1.16 +              handle UnequalLengths => NONE
    1.17                     | Term.TERM _ => NONE
    1.18          in
    1.19            (Seq.make (clean_unify' useq))