# HG changeset patch
# User wenzelm
# Date 1003170942 -7200
# Node ID bdd2ac7c75ff2ba59ed80b265202f2dcb8fc5dc1
# Parent  a08b62908caa868bf911996cb5644fb41a868a5b
ObjectLogic.rulify;

diff -r a08b62908caa -r bdd2ac7c75ff src/HOL/UNITY/Simple/NSP_Bad.ML
--- a/src/HOL/UNITY/Simple/NSP_Bad.ML	Mon Oct 15 20:35:10 2001 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.ML	Mon Oct 15 20:35:42 2001 +0200
@@ -12,7 +12,7 @@
 *)
 
 fun impOfAlways th =
-  rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
+  ObjectLogic.rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
 
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];