added option for specialisation to the predicate compiler

--- 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 = [],

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
@@ -107,6 +107,7 @@
     no_topmost_reordering : bool,
     function_flattening : bool,
     fail_safe_function_flattening : bool,
+    specialise : bool,
     no_higher_order_predicate : string list,
     inductify : bool,
     compilation : compilation
@@ -125,6 +126,7 @@
   val no_topmost_reordering : options -> bool
   val function_flattening : options -> bool
   val fail_safe_function_flattening : options -> bool
+  val specialise : options -> bool
   val no_higher_order_predicate : options -> string list
   val is_inductify : options -> bool
   val compilation : options -> compilation
@@ -665,6 +667,7 @@
   skip_proof : bool,
   no_topmost_reordering : bool,
   function_flattening : bool,
+  specialise : bool,
   fail_safe_function_flattening : bool,
   no_higher_order_predicate : string list,
   inductify : bool,
@@ -688,6 +691,7 @@
 
 fun function_flattening (Options opt) = #function_flattening opt
 fun fail_safe_function_flattening (Options opt) = #fail_safe_function_flattening opt
+fun specialise (Options opt) = #specialise opt
 fun no_topmost_reordering (Options opt) = #no_topmost_reordering opt
 fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt
 
@@ -709,6 +713,7 @@
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = false,
+  specialise = false,
   fail_safe_function_flattening = false,
   no_higher_order_predicate = [],
   inductify = false,
@@ -717,7 +722,7 @@
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
   "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
-  "no_topmost_reordering"]
+  "specialise", "no_topmost_reordering"]
 
 fun print_step options s =
   if show_steps options then tracing s else ()