# HG changeset patch
# User paulson
# Date 908789095 -7200
# Node ID 2df6fccf5719757bca513940079d3053cbd28ad1
# Parent  822db50b3ec56fcf88dc9379693881fbe3509266
fixed comment

diff -r 822db50b3ec5 -r 2df6fccf5719 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Mon Oct 19 11:24:24 1998 +0200
+++ b/src/HOL/UNITY/Client.ML	Mon Oct 19 11:24:55 1998 +0200
@@ -79,8 +79,9 @@
 qed "ask_bounded";
 
 
-(*Curiously, we no longer need to expand the program definition, and 
-  expanding it is extremely expensive!*)
+(*We no longer need constrains_tac to expand the program definition, and 
+  expanding it is extremely expensive!  Instead, Acts_Cli_Join_eq expands
+  the program.*)
 program_defs_ref := [];
 
 (*Safety property 2: clients return the right number of tokens*)
@@ -92,8 +93,7 @@
 by (Force_tac 1);
 by (subgoal_tac "rel s <= giv s'" 1);
 by (force_tac (claset(),
-	       simpset() delsimps [Acts_eq]
-			 addsimps [stable_def, constrains_def]) 2);
+	       simpset() addsimps [stable_def, constrains_def]) 2);
 by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
 (*we note that "rel" is local to Client*)
 by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));