# HG changeset patch
# User lcp
# Date 748263233 -7200
# Node ID 75e163863e16d2593ec9a78f61aab140f9f47260
# Parent  2695ba9b40f7fb85d888f7b88822c02e0b911bfb
test commit

diff -r 2695ba9b40f7 -r 75e163863e16 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Thu Sep 16 17:41:10 1993 +0200
+++ b/src/ZF/ROOT.ML	Fri Sep 17 12:53:53 1993 +0200
@@ -1,5 +1,4 @@
 (*  Title: 	ZF/ROOT
-    ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
@@ -25,6 +24,20 @@
 	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
   in  rs_aux 1 rlss  end;
 
+fun CHECK_SOLVED (Tactic tf) = 
+  Tactic (fn state => 
+    case Sequence.pull (tf state) of
+	None => error"DO_GOAL: tactic list failed"
+      | Some(x,_) => 
+		if has_fewer_prems 1 x then
+		    Sequence.cons(x, Sequence.null)
+		else (writeln"DO_GOAL: unsolved goals!!";
+		      writeln"Final proof state was ...";
+		      print_goals (!goals_limit) x;
+		      raise ERROR));
+
+fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
+
 print_depth 1;
 use_thy "zf";