Goal.conclude;

--- a/src/Pure/IsaPlanner/isand.ML	Fri Oct 21 18:14:49 2005 +0200
+++ b/src/Pure/IsaPlanner/isand.ML	Fri Oct 21 18:14:50 2005 +0200
@@ -378,9 +378,9 @@
           Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
 
       val minimal_th = 
-          (Library.foldl (fn ( th', sgthm) => 
+          Goal.conclude (Library.foldl (fn ( th', sgthm) => 
                           Drule.compose_single (sgthm, 1, th'))
-                      (th, sgthms)) RS Drule.rev_triv_goal;
+                      (th, sgthms));
 
       val allified_th = 
           minimal_th