src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

   val ascii_string_of_mode : mode -> string
   (* premises *)
   datatype indprem = Prem of term | Negprem of term | Sidecond of term
     | Generator of (string * typ)
   val dest_indprem : indprem -> term
+  val map_indprem : (term -> term) -> indprem -> indprem
   (* general syntactic functions *)
   val conjuncts : term -> term list
   val is_equationlike : thm -> bool
   val is_pred_equation : thm -> bool
   val is_intro : string -> thm -> bool

     function_flattening : bool,
     fail_safe_function_flattening : bool,
     specialise : bool,
     no_higher_order_predicate : string list,
     inductify : bool,
+    detect_switches : bool,
     compilation : compilation
   };
   val expected_modes : options -> (string * mode list) option
   val proposed_modes : options -> (string * mode list) option
   val proposed_names : options -> string -> mode -> string option

   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 detect_switches : options -> bool
   val compilation : options -> compilation
   val default_options : options
   val bool_options : string list
   val print_step : options -> string -> unit
   (* simple transformations *)

 
 fun dest_indprem (Prem t) = t
   | dest_indprem (Negprem t) = t
   | dest_indprem (Sidecond t) = t
   | dest_indprem (Generator _) = raise Fail "cannot destruct generator"
+
+fun map_indprem f (Prem t) = Prem (f t)
+  | map_indprem f (Negprem t) = Negprem (f t)
+  | map_indprem f (Sidecond t) = Sidecond (f t)
+  | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T))))
 
 (* general syntactic functions *)
 
 (*Like dest_conj, but flattens conjunctions however nested*)
 fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)

   function_flattening : bool,
   specialise : bool,
   fail_safe_function_flattening : bool,
   no_higher_order_predicate : string list,
   inductify : bool,
+  detect_switches : bool,
   compilation : compilation
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
 fun proposed_modes (Options opt) = #proposed_modes opt

 fun no_higher_order_predicate (Options opt) = #no_higher_order_predicate opt
 
 fun is_inductify (Options opt) = #inductify opt
 
 fun compilation (Options opt) = #compilation opt
+
+fun detect_switches (Options opt) = #detect_switches opt
 
 val default_options = Options {
   expected_modes = NONE,
   proposed_modes = NONE,
   proposed_names = [],

   function_flattening = false,
   specialise = false,
   fail_safe_function_flattening = false,
   no_higher_order_predicate = [],
   inductify = false,
+  detect_switches = true,
   compilation = Pred
 }
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
   "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
-  "specialise", "no_topmost_reordering"]
+  "detect_switches", "specialise", "no_topmost_reordering"]
 
 fun print_step options s =
   if show_steps options then tracing s else ()
 
 (* simple transformations *)