# 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;