--- 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 =