--- a/src/ZF/Inductive_ZF.thy Sat Mar 01 14:10:15 2008 +0100
+++ b/src/ZF/Inductive_ZF.thy Sat Mar 01 15:01:03 2008 +0100
@@ -42,9 +42,6 @@
setup DatatypeTactics.setup
ML_setup {*
-val iT = Ind_Syntax.iT
-and oT = FOLogic.oT;
-
structure Lfp =
struct
val oper = @{const lfp}