added new arg for print_tac
authorpaulson
Mon Dec 28 17:03:47 1998 +0100 (1998-12-28)
changeset 60544a4f6ad607a1
parent 6053 8a1059aa01f0
child 6055 fdf4638bf726
added new arg for print_tac
src/Sequents/prover.ML
     1.1 --- a/src/Sequents/prover.ML	Mon Dec 28 16:59:28 1998 +0100
     1.2 +++ b/src/Sequents/prover.ML	Mon Dec 28 17:03:47 1998 +0100
     1.3 @@ -106,7 +106,8 @@
     1.4  fun repeat_goal_tac (Pack(safes,unsafes)) = 
     1.5    let val restac  =    RESOLVE_THEN safes
     1.6        and lastrestac = RESOLVE_THEN unsafes;
     1.7 -      fun gtac i = restac gtac i  ORELSE  (print_tac THEN lastrestac gtac i)
     1.8 +      fun gtac i = restac gtac i  
     1.9 +	           ORELSE  (print_tac "" THEN lastrestac gtac i)
    1.10    in  gtac  end; 
    1.11  
    1.12