--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 21 12:10:52 2010 +0200
@@ -112,7 +112,10 @@
val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
val _ = print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...")
- val (intross9, thy3) = Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
+ val (intross9, thy3) =
+ if specialise options then
+ Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
+ else (intross8, thy2)
val _ = print_intross options thy3 "introduction rules after specialisations: " intross9
val intross10 = map_specs (map_filter (peephole_optimisation thy3)) intross9
val _ = print_intross options thy3 "introduction rules before registering: " intross10
@@ -154,6 +157,7 @@
show_caught_failures = false,
skip_proof = chk "skip_proof",
function_flattening = not (chk "no_function_flattening"),
+ specialise = chk "specialise",
fail_safe_function_flattening = false,
no_topmost_reordering = (chk "no_topmost_reordering"),
no_higher_order_predicate = [],