--- a/src/Pure/thm.ML Wed Sep 08 23:49:39 1999 +0200
+++ b/src/Pure/thm.ML Thu Sep 09 12:25:01 1999 +0200
@@ -1505,7 +1505,7 @@
in if eres_flg then eres(rev rAs)
else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
end;
-end; (*open Sequence*)
+end;
fun bicompose match arg i state =