--- a/src/ZF/Datatype_ZF.thy Wed Jul 15 23:11:57 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy Wed Jul 15 23:48:21 2009 +0200
@@ -1,8 +1,6 @@
(* Title: ZF/Datatype.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-
*)
header{*Datatype and CoDatatype Definitions*}
@@ -103,7 +101,7 @@
handle Match => NONE;
- val conv = Simplifier.simproc (the_context ()) "data_free" ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
end;