src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Wed Apr 02 15:36:32 1997 +0200
+++ b/src/ZF/simpdata.ML	Wed Apr 02 15:37:35 1997 +0200
@@ -10,7 +10,7 @@
 
 (*For proving rewrite rules*)
 fun prove_fun s = 
-    (writeln s;  prove_goal thy s
+    (writeln s;  prove_goal ZF.thy s
        (fn prems => [ (cut_facts_tac prems 1), (Fast_tac 1) ]));
 
 (*Are all these really suitable?*)