--- a/src/ZF/simpdata.ML Mon Aug 17 13:06:29 1998 +0200
+++ b/src/ZF/simpdata.ML Mon Aug 17 13:09:08 1998 +0200
@@ -10,7 +10,7 @@
local
(*For proving rewrite rules*)
- fun prover s = (prove_goal ZF.thy s (fn _ => [Blast_tac 1]));
+ fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
in