# HG changeset patch
# User wenzelm
# Date 1129911290 -7200
# Node ID a84ac7c201ea6e2c6218a45169af1e6346359c1e
# Parent  7262f4a4519020c918b5462bae7f027bddf59e60
Goal.conclude;

diff -r 7262f4a45190 -r a84ac7c201ea src/Pure/IsaPlanner/isand.ML
--- 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