diff -r f67607c3e56e -r 6199df39688d src/Pure/Tools/compute.ML
--- a/src/Pure/Tools/compute.ML	Sun Apr 15 14:32:04 2007 +0200
+++ b/src/Pure/Tools/compute.ML	Sun Apr 15 14:32:05 2007 +0200
@@ -163,7 +163,7 @@
 
         fun thm2rule table invtable ccount th =
             let
-                val prop = Drule.plain_prop_of th
+                val prop = Thm.plain_prop_of th
                   handle THM _ => raise (Make "theorems must be plain propositions")
                 val (a, b) = Logic.dest_equals prop
                   handle TERM _ => raise (Make "theorems must be meta-level equations")