--- a/src/HOL/HOL.thy Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/HOL.thy Wed Sep 23 16:20:12 2009 +0200
@@ -2023,13 +2023,7 @@
subsection {* Preprocessing for the predicate compiler *}
-ML {*
-structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
-(
- val name = "predicate_compile_preproc_const_def"
- val description = "definitions of constants as needed by the preprocessing for the predicate compiler "
-)
-*}
+setup {* Predicate_Compile_Preproc_Const_Defs.setup *}
subsection {* Nitpick setup *}