src/Pure/thm.ML

--- a/src/Pure/thm.ML	Wed Apr 26 22:38:11 2006 +0200
+++ b/src/Pure/thm.ML	Wed Apr 26 22:38:16 2006 +0200
@@ -1429,7 +1429,7 @@
                  hyps = union_hyps rhyps shyps,
                  tpairs = ntpairs,
                  prop = Logic.list_implies normp}
-        in  Seq.cons(th, thq)  end  handle COMPOSE => thq;
+        in  Seq.cons th thq  end  handle COMPOSE => thq;
      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop)
        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)