# HG changeset patch
# User paulson
# Date 914861027 -3600
# Node ID 4a4f6ad607a1de09bb6511af8c13302099687d64
# Parent  8a1059aa01f084a93b721eb7f5db660d30a928f6
added new arg for print_tac

diff -r 8a1059aa01f0 -r 4a4f6ad607a1 src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Mon Dec 28 16:59:28 1998 +0100
+++ b/src/Sequents/prover.ML	Mon Dec 28 17:03:47 1998 +0100
@@ -106,7 +106,8 @@
 fun repeat_goal_tac (Pack(safes,unsafes)) = 
   let val restac  =    RESOLVE_THEN safes
       and lastrestac = RESOLVE_THEN unsafes;
-      fun gtac i = restac gtac i  ORELSE  (print_tac THEN lastrestac gtac i)
+      fun gtac i = restac gtac i  
+	           ORELSE  (print_tac "" THEN lastrestac gtac i)
   in  gtac  end;