# HG changeset patch
# User paulson
# Date 878385780 -3600
# Node ID 7b508ac609f70b01709be1187eb51a1aac57ebeb
# Parent  8862fcb5d44acb6a7bc2b84d6156497716a8565b
Fixed comments

diff -r 8862fcb5d44a -r 7b508ac609f7 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Nov 01 13:02:39 1997 +0100
+++ b/src/Provers/classical.ML	Sat Nov 01 13:03:00 1997 +0100
@@ -568,13 +568,14 @@
 
 (*** Unsafe steps instantiate variables or lose information ***)
 
-(*But these unsafe steps at least solve a subgoal!*)
+(*Backtracking is allowed among the various these unsafe ways of
+  proving a subgoal.  *)
 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   assume_tac 			  APPEND' 
   contr_tac 			  APPEND' 
   biresolve_from_nets_tac safe0_netpair;
 
-(*These are much worse since they could generate more and more subgoals*)
+(*These unsafe steps could generate more subgoals.*)
 fun instp_step_tac (CS{safep_netpair,...}) =
   biresolve_from_nets_tac safep_netpair;