# HG changeset patch
# User paulson
# Date 859988255 -7200
# Node ID 02c12d4c8b97ef13db39b5efff60a09e61ebd510
# Parent  6e3ccb94836c07bf4cb7e6c4416f31e70a045ef1
Uses ZF.thy again, to make that theory usable

diff -r 6e3ccb94836c -r 02c12d4c8b97 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?*)