src/HOL/Auth/Event.ML

--- a/src/HOL/Auth/Event.ML	Wed Sep 24 10:51:52 1997 +0200
+++ b/src/HOL/Auth/Event.ML	Wed Sep 24 12:24:41 1997 +0200
@@ -82,7 +82,9 @@
 	      (!simpset addsimps [parts_insert_spies]
 	                setloop split_tac [expand_event_case, expand_if])));
 by (ALLGOALS Blast_tac);
-bind_thm ("usedI", impOfSubs (result()));
+qed "parts_spies_subset_used";
+
+bind_thm ("usedI", impOfSubs parts_spies_subset_used);
 AddIs [usedI];
 
 goal thy "parts (initState B) <= used evs";