# HG changeset patch
# User paulson
# Date 835108564 -7200
# Node ID 89f8d4a88cca201bc4ec500ed045f5324e7a87d9
# Parent  23bda45846a2c72e5b1a35bf768f660ca8239ef3
Addition of Safe_step_tac

diff -r 23bda45846a2 -r 89f8d4a88cca src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jun 18 16:27:04 1996 +0200
+++ b/src/Provers/classical.ML	Tue Jun 18 16:36:04 1996 +0200
@@ -94,6 +94,7 @@
   val AddSEs		: thm list -> unit
   val AddSIs		: thm list -> unit
   val Delrules		: thm list -> unit
+  val Safe_step_tac	: int -> tactic
   val Step_tac 		: int -> tactic
   val Fast_tac 		: int -> tactic
   val Best_tac 		: int -> tactic
@@ -557,6 +558,8 @@
 
 (*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*)
 
+fun Safe_step_tac i = safe_step_tac (!claset) i; 
+
 fun Step_tac i = step_tac (!claset) i; 
 
 fun Fast_tac i = fast_tac (!claset) i;