src/HOL/UNITY/Client.ML
changeset 7537 875754b599df
parent 7361 477e1bdf230f
child 7594 8a188ef6545e
--- a/src/HOL/UNITY/Client.ML	Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Client.ML	Fri Sep 10 18:40:06 1999 +0200
@@ -90,7 +90,7 @@
 \                       size (rel s) = k & ask s ! k <= giv s ! k}";
 by (res_inst_tac [("act", "rel_act")] transient_mem 1);
 by (auto_tac (claset(),
-	      simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def]));
+	      simpset() addsimps [Domain_def, Cli_prg_def]));
 qed "transient_lemma";