src/ZF/Datatype.ML

--- a/src/ZF/Datatype.ML	Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/Datatype.ML	Wed Jan 15 16:45:32 2003 +0100
@@ -97,7 +97,8 @@
 
 
  val conv = 
-     Simplifier.simproc (Theory.sign_of ZF.thy) "data_free" ["(x::i) = y"] proc;
+     Simplifier.simproc (Theory.sign_of (theory "ZF")) "data_free" 
+                        ["(x::i) = y"] proc;
 end;