--- a/src/HOL/Tools/inductive_set_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -543,14 +543,12 @@
val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
-val inductive_setP =
+val _ =
OuterSyntax.command "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
-val coinductive_setP =
+val _ =
OuterSyntax.command "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
-val _ = OuterSyntax.add_parsers [inductive_setP, coinductive_setP];
-
end;
end;