src/HOL/UNITY/NSP_Bad.ML

--- a/src/HOL/UNITY/NSP_Bad.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -11,9 +11,8 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-fun impOfAlways th = 
-    normalize_thm [RSspec,RSmp]
-       (th RS Always_includes_reachable RS subsetD RS CollectD);
+fun impOfAlways th =
+  rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
 
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];