src/HOL/HOL.thy

 
 quickcheck_params [size = 5, iterations = 50]
 
 subsection {* Preprocessing for the predicate compiler *}
 
-setup {* Predicate_Compile_Preproc_Const_Defs.setup *}
+ML {*
+structure Predicate_Compile_Alternative_Defs = Named_Thms
+(
+  val name = "code_pred_def"
+  val description = "alternative definitions of constants for the Predicate Compiler"
+)
+*}
+
+ML {*
+structure Predicate_Compile_Inline_Defs = Named_Thms
+(
+  val name = "code_pred_inline"
+  val description = "inlining definitions for the Predicate Compiler"
+)
+*}
+
+setup {*
+  Predicate_Compile_Alternative_Defs.setup
+  #> Predicate_Compile_Inline_Defs.setup
+  #> Predicate_Compile_Preproc_Const_Defs.setup
+*}
 
 subsection {* Nitpick setup *}
 
 text {* This will be relocated once Nitpick is moved to HOL. *}