# HG changeset patch
# User wenzelm
# Date 1392208385 -3600
# Node ID 3fd63b92ea3bc020d113d3df047bd4919905df15
# Parent  9781e17dcc23d57b308d5f622c6bae0ec4f017be
tuned whitespace;

diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -18,9 +18,9 @@
   val set_ensure_groundness : code_options -> code_options
   val map_limit_predicates : ((string list * int) list -> (string list * int) list)
     -> code_options -> code_options
-  val code_options_of : theory -> code_options 
+  val code_options_of : theory -> code_options
   val map_code_options : (code_options -> code_options) -> theory -> theory
-  
+
   datatype arith_op = Plus | Minus
   datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
     | Number of int | ArithOp of arith_op * prol_term list;
@@ -33,20 +33,20 @@
   type clause = ((string * prol_term list) * prem);
   type logic_program = clause list;
   type constant_table = (string * string) list
-  
+
   val generate : Predicate_Compile_Aux.mode option * bool ->
     Proof.context -> string -> (logic_program * constant_table)
   val write_program : logic_program -> string
   val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) ->
     string list -> int option -> prol_term list list
-  
+
   val active : bool Config.T
   val test_goals :
     Proof.context -> bool -> (string * typ) list -> (term * term list) list ->
       Quickcheck.result list
 
   val trace : bool Unsynchronized.ref
-  
+
   val replace : ((string * string) * string) -> logic_program -> logic_program
 end;
 
@@ -57,11 +57,11 @@
 
 val trace = Unsynchronized.ref false
 
-fun tracing s = if !trace then Output.tracing s else () 
+fun tracing s = if !trace then Output.tracing s else ()
+
 
 (* code generation options *)
 
-
 type code_options =
   {ensure_groundness : bool,
    limit_globally : int option,
@@ -79,15 +79,15 @@
 
 fun map_limit_predicates f {ensure_groundness, limit_globally, limited_types, limited_predicates,
   replacing, manual_reorder} =
-  {ensure_groundness = ensure_groundness, limit_globally = limit_globally, limited_types = limited_types,
-   limited_predicates = f limited_predicates, replacing = replacing,
-   manual_reorder = manual_reorder}
+  {ensure_groundness = ensure_groundness, limit_globally = limit_globally,
+   limited_types = limited_types, limited_predicates = f limited_predicates,
+   replacing = replacing, manual_reorder = manual_reorder}
 
 fun merge_global_limit (NONE, NONE) = NONE
   | merge_global_limit (NONE, SOME n) = SOME n
   | merge_global_limit (SOME n, NONE) = SOME n
   | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))  (* FIXME odd merge *)
-   
+
 structure Options = Theory_Data
 (
   type T = code_options
@@ -113,6 +113,7 @@
 
 val map_code_options = Options.map
 
+
 (* system configuration *)
 
 datatype prolog_system = SWI_PROLOG | YAP
@@ -121,7 +122,7 @@
   | string_of_system YAP = "yap"
 
 type system_configuration = {timeout : Time.time, prolog_system : prolog_system}
-                                                
+
 structure System_Config = Generic_Data
 (
   type T = system_configuration
@@ -130,11 +131,13 @@
   fun merge (a, _) = a
 )
 
+
 (* general string functions *)
 
 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
 
+
 (* internal program representation *)
 
 datatype arith_op = Plus | Minus
@@ -153,7 +156,7 @@
   | map_vars f (ArithOp (opr, ts)) = ArithOp (opr, map (map_vars f) ts)
   | map_vars f (AppF (fs, ts)) = AppF (fs, map (map_vars f) ts)
   | map_vars f t = t
-  
+
 fun maybe_AppF (c, []) = Cons c
   | maybe_AppF (c, xs) = AppF (c, xs)
 
@@ -167,7 +170,7 @@
 
 fun string_of_prol_term (Var s) = "Var " ^ s
   | string_of_prol_term (Cons s) = "Cons " ^ s
-  | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" 
+  | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")"
   | string_of_prol_term (Number n) = "Number " ^ string_of_int n
 
 datatype prem = Conj of prem list
@@ -195,11 +198,12 @@
   | fold_prem_terms f (ArithEq (l, r)) = f l #> f r
   | fold_prem_terms f (NotArithEq (l, r)) = f l #> f r
   | fold_prem_terms f (Ground (v, T)) = f (Var v)
-  
+
 type clause = ((string * prol_term list) * prem);
 
 type logic_program = clause list;
- 
+
+
 (* translation from introduction rules to internal representation *)
 
 fun mk_conform f empty avoid name =
@@ -211,6 +215,7 @@
     val name'' = f (if name' = "" then empty else name')
   in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
 
+
 (** constant table **)
 
 type constant_table = (string * string) list
@@ -227,11 +232,11 @@
   in
     fold update' consts constant_table
   end
-  
+
 fun translate_const constant_table c =
-  case AList.lookup (op =) constant_table c of
+  (case AList.lookup (op =) constant_table c of
     SOME c' => c'
-  | NONE => error ("No such constant: " ^ c)
+  | NONE => error ("No such constant: " ^ c))
 
 fun inv_lookup _ [] _ = NONE
   | inv_lookup eq ((key, value)::xs) value' =
@@ -239,9 +244,10 @@
       else inv_lookup eq xs value';
 
 fun restore_const constant_table c =
-  case inv_lookup (op =) constant_table c of
+  (case inv_lookup (op =) constant_table c of
     SOME c' => c'
-  | NONE => error ("No constant corresponding to "  ^ c)
+  | NONE => error ("No constant corresponding to "  ^ c))
+
 
 (** translation of terms, literals, premises, and clauses **)
 
@@ -256,52 +262,53 @@
   in funpow n (fn t => AppF (Suc, [t])) (Cons zero) end
 
 fun translate_term ctxt constant_table t =
-  case try HOLogic.dest_number t of
+  (case try HOLogic.dest_number t of
     SOME (@{typ "int"}, n) => Number n
   | SOME (@{typ "nat"}, n) => mk_nat_term constant_table n
   | NONE =>
       (case strip_comb t of
-        (Free (v, T), []) => Var v 
+        (Free (v, T), []) => Var v
       | (Const (c, _), []) => Cons (translate_const constant_table c)
       | (Const (c, _), args) =>
-        (case translate_arith_const c of
-          SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
-        | NONE =>                                                             
-            AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
-      | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
+          (case translate_arith_const c of
+            SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
+          | NONE =>
+              AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
+      | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t)))
 
 fun translate_literal ctxt constant_table t =
-  case strip_comb t of
+  (case strip_comb t of
     (Const (@{const_name HOL.eq}, _), [l, r]) =>
       let
         val l' = translate_term ctxt constant_table l
         val r' = translate_term ctxt constant_table r
       in
-        (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) (l', r')
+        (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq)
+          (l', r')
       end
   | (Const (c, _), args) =>
       Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
-  | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
+  | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t))
 
 fun NegRel_of (Rel lit) = NotRel lit
   | NegRel_of (Eq eq) = NotEq eq
   | NegRel_of (ArithEq eq) = NotArithEq eq
 
 fun mk_groundness_prems t = map Ground (Term.add_frees t [])
-  
-fun translate_prem ensure_groundness ctxt constant_table t =  
-    case try HOLogic.dest_not t of
-      SOME t =>
-        if ensure_groundness then
-          Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
-        else
-          NegRel_of (translate_literal ctxt constant_table t)
-    | NONE => translate_literal ctxt constant_table t
-    
+
+fun translate_prem ensure_groundness ctxt constant_table t =
+  (case try HOLogic.dest_not t of
+    SOME t =>
+      if ensure_groundness then
+        Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
+      else
+        NegRel_of (translate_literal ctxt constant_table t)
+  | NONE => translate_literal ctxt constant_table t)
+
 fun imp_prems_conv cv ct =
-  case Thm.term_of ct of
+  (case Thm.term_of ct of
     Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
-  | _ => Conv.all_conv ct
+  | _ => Conv.all_conv ct)
 
 fun preprocess_intro thy rule =
   Conv.fconv_rule
@@ -330,17 +337,17 @@
 
 fun add_edges edges_of key G =
   let
-    fun extend' key (G, visited) = 
-      case try (Graph.get_node G) key of
-          SOME v =>
-            let
-              val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v))
-              val (G', visited') = fold extend'
-                (subtract (op =) (key :: visited) new_edges) (G, key :: visited)
-            in
-              (fold (Graph.add_edge o (pair key)) new_edges G', visited')
-            end
-        | NONE => (G, visited)
+    fun extend' key (G, visited) =
+      (case try (Graph.get_node G) key of
+        SOME v =>
+          let
+            val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v))
+            val (G', visited') = fold extend'
+              (subtract (op =) (key :: visited) new_edges) (G, key :: visited)
+          in
+            (fold (Graph.add_edge o (pair key)) new_edges G', visited')
+          end
+      | NONE => (G, visited))
   in
     fst (extend' key (G, []))
   end
@@ -350,6 +357,7 @@
     "Constant " ^ const ^ "has intros:\n" ^
     cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
 
+
 (* translation of moded predicates *)
 
 (** generating graph of moded predicates **)
@@ -361,15 +369,20 @@
       (case fst (strip_comb t) of
         Const (c, _) => SOME (c, (pol, Predicate_Compile_Core.head_mode_of derivation))
       | _ => NONE)
-    fun req (Predicate_Compile_Aux.Prem t, derivation) = req_mode_of polarity (t, derivation)
-      | req (Predicate_Compile_Aux.Negprem t, derivation) = req_mode_of (not polarity) (t, derivation)
+    fun req (Predicate_Compile_Aux.Prem t, derivation) =
+          req_mode_of polarity (t, derivation)
+      | req (Predicate_Compile_Aux.Negprem t, derivation) =
+          req_mode_of (not polarity) (t, derivation)
       | req _ = NONE
-  in      
+  in
     maps (fn (_, prems) => map_filter req prems) cls
   end
- 
-structure Mode_Graph = Graph(type key = string * (bool * Predicate_Compile_Aux.mode)
-  val ord = prod_ord fast_string_ord (prod_ord bool_ord Predicate_Compile_Aux.mode_ord));
+
+structure Mode_Graph =
+  Graph(
+    type key = string * (bool * Predicate_Compile_Aux.mode)
+    val ord = prod_ord fast_string_ord (prod_ord bool_ord Predicate_Compile_Aux.mode_ord)
+  )
 
 fun mk_moded_clauses_graph ctxt scc gr =
   let
@@ -386,14 +399,16 @@
           Predicate_Compile_Core.prepare_intrs options ctxt prednames
             (maps (Core_Data.intros_of ctxt) prednames)
         val ((moded_clauses, random'), _) =
-          Mode_Inference.infer_modes mode_analysis_options options 
+          Mode_Inference.infer_modes mode_analysis_options options
             (lookup_modes, lookup_neg_modes, needs_random) ctxt preds all_modes param_vs clauses
         val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
         val pos_modes' = map (apsnd (map_filter (fn (true, m) => SOME m | _ => NONE))) modes
         val neg_modes' = map (apsnd (map_filter (fn (false, m) => SOME m | _ => NONE))) modes
-        val _ = tracing ("Inferred modes:\n" ^
-          cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
-            (fn (p, m) => Predicate_Compile_Aux.string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
+        val _ =
+          tracing ("Inferred modes:\n" ^
+            cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
+              (fn (p, m) =>
+                Predicate_Compile_Aux.string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
         val gr' = gr
           |> fold (fn (p, mps) => fold (fn (mode, cls) =>
                 Mode_Graph.new_node ((p, mode), cls)) mps)
@@ -406,8 +421,8 @@
           AList.merge (op =) (op =) (neg_modes, neg_modes'),
           AList.merge (op =) (op =) (random, random')))
       end
-  in  
-    fst (fold infer (rev scc) (Mode_Graph.empty, ([], [], []))) 
+  in
+    fst (fold infer (rev scc) (Mode_Graph.empty, ([], [], [])))
   end
 
 fun declare_moded_predicate moded_preds table =
@@ -431,32 +446,34 @@
     fun mk_literal pol derivation constant_table' t =
       let
         val (p, args) = strip_comb t
-        val mode = Predicate_Compile_Core.head_mode_of derivation 
+        val mode = Predicate_Compile_Core.head_mode_of derivation
         val name = fst (dest_Const p)
-        
+
         val p' = the (AList.lookup (op =) moded_pred_table' (name, (pol, mode)))
         val args' = map (translate_term ctxt constant_table') args
       in
         Rel (p', args')
       end
     fun mk_prem pol (indprem, derivation) constant_table =
-      case indprem of
+      (case indprem of
         Predicate_Compile_Aux.Generator (s, T) => (Ground (s, T), constant_table)
       | _ =>
-        declare_consts (Term.add_const_names (Predicate_Compile_Aux.dest_indprem indprem) []) constant_table
+        declare_consts (Term.add_const_names (Predicate_Compile_Aux.dest_indprem indprem) [])
+          constant_table
         |> (fn constant_table' =>
           (case indprem of Predicate_Compile_Aux.Negprem t =>
             NegRel_of (mk_literal (not pol) derivation constant_table' t)
           | _ =>
-            mk_literal pol derivation constant_table' (Predicate_Compile_Aux.dest_indprem indprem), constant_table'))
+            mk_literal pol derivation constant_table' (Predicate_Compile_Aux.dest_indprem indprem),
+              constant_table')))
     fun mk_clause pred_name pol (ts, prems) (prog, constant_table) =
-    let
-      val constant_table' = declare_consts (fold Term.add_const_names ts []) constant_table
-      val args = map (translate_term ctxt constant_table') ts
-      val (prems', constant_table'') = fold_map (mk_prem pol) prems constant_table'
-    in
-      (((pred_name, args), Conj prems') :: prog, constant_table'')
-    end
+      let
+        val constant_table' = declare_consts (fold Term.add_const_names ts []) constant_table
+        val args = map (translate_term ctxt constant_table') ts
+        val (prems', constant_table'') = fold_map (mk_prem pol) prems constant_table'
+      in
+        (((pred_name, args), Conj prems') :: prog, constant_table'')
+      end
     fun mk_clauses (pred, mode as (pol, _)) =
       let
         val clauses = Mode_Graph.get_node moded_gr (pred, mode)
@@ -469,35 +486,37 @@
   end
 
 fun generate (use_modes, ensure_groundness) ctxt const =
-  let 
+  let
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
     val gr = Core_Data.intros_graph_of ctxt
     val gr' = add_edges depending_preds_of const gr
     val scc = strong_conn_of gr' [const]
-    val initial_constant_table = 
+    val initial_constant_table =
       declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}] []
   in
-    case use_modes of
+    (case use_modes of
       SOME mode =>
         let
           val moded_gr = mk_moded_clauses_graph ctxt scc gr
           val moded_gr' = Mode_Graph.restrict
             (member (op =) (Mode_Graph.all_succs moded_gr [(const, (true, mode))])) moded_gr
-          val scc = Mode_Graph.strong_conn moded_gr' 
+          val scc = Mode_Graph.strong_conn moded_gr'
         in
           apfst rev (apsnd snd
             (fold (mk_program ctxt moded_gr') (rev scc) ([], ([], initial_constant_table))))
         end
-      | NONE =>
-        let 
+    | NONE =>
+        let
           val _ = print_intros ctxt gr (flat scc)
           val constant_table = declare_consts (flat scc) initial_constant_table
         in
-          apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
-        end
+          apfst flat
+            (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
+        end)
   end
-  
+
+
 (* implementation for fully enumerating predicates and
   for size-limited predicates for enumerating the values of a datatype upto a specific size *)
 
@@ -506,7 +525,7 @@
   | add_ground_typ _ = I
 
 fun mk_relname (Type (Tcon, Targs)) =
-  first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
+      first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
   | mk_relname _ = raise Fail "unexpected type"
 
 fun mk_lim_relname T = "lim_" ^  mk_relname T
@@ -519,14 +538,15 @@
   | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
 
 fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T
-  
+
 fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) =
   if member (op =) seen T then ([], (seen, constant_table))
   else
     let
-      val (limited, size) = case AList.lookup (op =) limited_types T of
-        SOME s => (true, s)
-      | NONE => (false, 0)      
+      val (limited, size) =
+        (case AList.lookup (op =) limited_types T of
+          SOME s => (true, s)
+        | NONE => (false, 0))
       val rel_name = (if limited then mk_lim_relname else mk_relname) T
       fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) =
         let
@@ -537,9 +557,9 @@
           val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts))
           val lim_var =
             if limited then
-              if recursive then [AppF ("suc", [Var "Lim"])]              
+              if recursive then [AppF ("suc", [Var "Lim"])]
               else [Var "Lim"]
-            else [] 
+            else []
           fun mk_prem v T' =
             if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v])
             else Rel (mk_relname T', [v])
@@ -565,18 +585,20 @@
 
 fun replace_ground (Conj prems) = Conj (map replace_ground prems)
   | replace_ground (Ground (x, T)) =
-    Rel (mk_relname T, [Var x])  
+    Rel (mk_relname T, [Var x])
   | replace_ground p = p
-  
+
 fun add_ground_predicates ctxt limited_types (p, constant_table) =
   let
     val ground_typs = fold (add_ground_typ o snd) p []
-    val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table)
+    val (grs, (_, constant_table')) =
+      fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table)
     val p' = map (apsnd replace_ground) p
   in
     ((flat grs) @ p', constant_table')
   end
 
+
 (* make depth-limited version of predicate *)
 
 fun mk_lim_rel_name rel_name = "lim_" ^ rel_name
@@ -600,8 +622,8 @@
 fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
 
 fun add_limited_predicates limited_predicates (p, constant_table) =
-  let                                     
-    fun add (rel_names, limit) p = 
+  let
+    fun add (rel_names, limit) p =
       let
         val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
         val clauses' = map (mk_depth_limited rel_names) clauses
@@ -609,7 +631,7 @@
           let
             val nargs = length (snd (fst
               (the (find_first (fn ((rel, _), _) => rel = rel_name) clauses))))
-            val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)        
+            val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
           in
             (("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
           end
@@ -629,10 +651,12 @@
           if rel = from then Rel (to, ts) else r
       | replace_prem r = r
   in
-    map (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem)) p
+    map
+      (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem))
+      p
   end
 
-  
+
 (* reorder manually : reorder premises of ith clause of predicate p by a permutation perm *)
 
 fun reorder_manually reorder p =
@@ -642,14 +666,16 @@
         val seen' = AList.map_default (op =) (rel, 0) (fn x => x + 1) seen
         val i = the (AList.lookup (op =) seen' rel)
         val perm = AList.lookup (op =) reorder (rel, i)
-        val prem' = (case perm of 
-          SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem)
-        | NONE => prem)
+        val prem' =
+          (case perm of
+            SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem)
+          | NONE => prem)
       in (((rel, args), prem'), seen') end
   in
     fst (fold_map reorder' p [])
   end
 
+
 (* rename variables to prolog-friendly names *)
 
 fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
@@ -658,7 +684,7 @@
 
 fun is_prolog_conform v =
   forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v)
-  
+
 fun mk_renaming v renaming =
   (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
 
@@ -667,9 +693,10 @@
     val vars = fold_prem_terms add_vars prem (fold add_vars args [])
     val renaming = fold mk_renaming vars []
   in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end
-  
+
 val rename_vars_program = map rename_vars_clause
 
+
 (* limit computation globally by some threshold *)
 
 fun limit_globally ctxt limit const_name (p, constant_table) =
@@ -686,6 +713,7 @@
     (entry_clause :: p' @ p'', constant_table)
   end
 
+
 (* post processing of generated prolog program *)
 
 fun post_process ctxt options const_name (p, constant_table) =
@@ -703,6 +731,7 @@
   |> apfst (reorder_manually (#manual_reorder options))
   |> apfst rename_vars_program
 
+
 (* code printer *)
 
 fun write_arith_op Plus = "+"
@@ -710,15 +739,17 @@
 
 fun write_term (Var v) = v
   | write_term (Cons c) = c
-  | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
-  | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
+  | write_term (AppF (f, args)) =
+      f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
+  | write_term (ArithOp (oper, [a1, a2])) =
+      write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
   | write_term (Number n) = string_of_int n
 
 fun write_rel (pred, args) =
-  pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
+  pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
 
 fun write_prem (Conj prems) = space_implode ", " (map write_prem prems)
-  | write_prem (Rel p) = write_rel p  
+  | write_prem (Rel p) = write_rel p
   | write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
   | write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
   | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
@@ -730,7 +761,8 @@
   write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
 
 fun write_program p =
-  cat_lines (map write_clause p) 
+  cat_lines (map write_clause p)
+
 
 (* query templates *)
 
@@ -740,7 +772,7 @@
   "eval :- once("  ^ rel ^ "(" ^ space_implode ", " (map write_term args) ^ ")),\n" ^
   "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
   "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
-  
+
 fun swi_prolog_query_firstn n (rel, args) vnames =
   "eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
     rel ^ "(" ^ space_implode ", " (map write_term args) ^ "), Sols), writelist(Sols).\n" ^
@@ -748,7 +780,7 @@
     "writelist([(" ^ space_implode ", " vnames ^ ")|SolutionTail]) :- " ^
     "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
     "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(SolutionTail).\n"
-  
+
 val swi_prolog_prelude =
   ":- use_module(library('dialect/ciao/aggregates')).\n" ^
   ":- style_check(-singleton).\n" ^
@@ -757,6 +789,7 @@
   "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
   "main :- halt(1).\n"
 
+
 (** query and prelude for yap **)
 
 fun yap_query_first (rel, args) vnames =
@@ -767,18 +800,25 @@
 val yap_prelude =
   ":- initialization(eval).\n"
 
+
 (* system-dependent query, prelude and invocation *)
 
-fun query system nsols = 
-  case system of
+fun query system nsols =
+  (case system of
     SWI_PROLOG =>
-      (case nsols of NONE => swi_prolog_query_first | SOME n => swi_prolog_query_firstn n)
+      (case nsols of
+        NONE => swi_prolog_query_first
+      | SOME n => swi_prolog_query_firstn n)
   | YAP =>
-      case nsols of NONE => yap_query_first | SOME n =>
-        error "No support for querying multiple solutions in the prolog system yap"
+      (case nsols of
+        NONE => yap_query_first
+      | SOME n =>
+          error "No support for querying multiple solutions in the prolog system yap"))
 
 fun prelude system =
-  case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
+  (case system of
+    SWI_PROLOG => swi_prolog_prelude
+  | YAP => yap_prelude)
 
 fun invoke system file =
   let
@@ -804,7 +844,8 @@
   Scan.many1 Symbol.is_ascii_digit
 
 val scan_atom =
-  Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
+  Scan.many1
+    (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
 
 val scan_var =
   Scan.many1
@@ -821,7 +862,8 @@
 val is_atom_ident = forall Symbol.is_ascii_lower
 
 val is_var_ident =
-  forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
+  forall (fn s =>
+    Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
 
 fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0
 
@@ -837,23 +879,25 @@
 val parse_term = fst o Scan.finite Symbol.stopper
     (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
   o raw_explode
-  
+
 fun parse_solutions sol =
   let
-    fun dest_eq s = case space_explode "=" s of
+    fun dest_eq s =
+      (case space_explode "=" s of
         (l :: r :: []) => parse_term (unprefix " " r)
-      | _ => raise Fail "unexpected equation in prolog output"
+      | _ => raise Fail "unexpected equation in prolog output")
     fun parse_solution s = map dest_eq (space_explode ";" s)
-    val sols = case space_explode "\n" sol of [] => [] | s => fst (split_last s)  
+    val sols = (case space_explode "\n" sol of [] => [] | s => fst (split_last s))
   in
     map parse_solution sols
-  end 
-  
+  end
+
+
 (* calling external interpreter and getting results *)
 
 fun run (timeout, system) p (query_rel, args) vnames nsols =
   let
-    val renaming = fold mk_renaming (fold add_vars args vnames) [] 
+    val renaming = fold mk_renaming (fold add_vars args vnames) []
     val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
     val args' = map (rename_vars_term renaming) args
     val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
@@ -867,26 +911,27 @@
     tss
   end
 
+
 (* restoring types in terms *)
 
 fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
   | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
-  | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number") 
+  | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number")
   | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
   | restore_term ctxt constant_table (AppF (f, args), T) =
-    let
-      val thy = Proof_Context.theory_of ctxt
-      val c = restore_const constant_table f
-      val cT = Sign.the_const_type thy c
-      val (argsT, resT) = strip_type cT
-      val subst = Sign.typ_match thy (resT, T) Vartab.empty
-      val argsT' = map (Envir.subst_type subst) argsT
-    in
-      list_comb (Const (c, Envir.subst_type subst cT),
-        map (restore_term ctxt constant_table) (args ~~ argsT'))
-    end
+      let
+        val thy = Proof_Context.theory_of ctxt
+        val c = restore_const constant_table f
+        val cT = Sign.the_const_type thy c
+        val (argsT, resT) = strip_type cT
+        val subst = Sign.typ_match thy (resT, T) Vartab.empty
+        val argsT' = map (Envir.subst_type subst) argsT
+      in
+        list_comb (Const (c, Envir.subst_type subst cT),
+          map (restore_term ctxt constant_table) (args ~~ argsT'))
+      end
 
-    
+
 (* restore numerals in natural numbers *)
 
 fun restore_nat_numerals t =
@@ -894,9 +939,10 @@
     HOLogic.mk_number @{typ nat} (HOLogic.dest_nat t)
   else
     (case t of
-        t1 $ t2 => restore_nat_numerals t1 $ restore_nat_numerals t2
-      | t => t)
-  
+      t1 $ t2 => restore_nat_numerals t1 $ restore_nat_numerals t2
+    | t => t)
+
+
 (* values command *)
 
 val preprocess_options = Predicate_Compile_Aux.Options {
@@ -926,17 +972,19 @@
 fun values ctxt soln t_compr =
   let
     val options = code_options_of (Proof_Context.theory_of ctxt)
-    val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
-      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
-    val (body, Ts, fp) = HOLogic.strip_psplits split;
+    val split =
+      (case t_compr of
+        (Const (@{const_name Collect}, _) $ t) => t
+      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
+    val (body, Ts, fp) = HOLogic.strip_psplits split
     val output_names = Name.variant_list (Term.add_free_names body [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
     val output_frees = rev (map2 (curry Free) output_names Ts)
     val body = subst_bounds (output_frees, body)
     val (pred as Const (name, T), all_args) =
-      case strip_comb body of
+      (case strip_comb body of
         (Const (name, T), all_args) => (Const (name, T), all_args)
-      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
+      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head))
     val _ = tracing "Preprocessing specification..."
     val T = Sign.the_const_type (Proof_Context.theory_of ctxt) name
     val t = Const (name, T)
@@ -956,7 +1004,7 @@
     val _ = tracing "Restoring terms..."
     val empty = Const(@{const_name bot}, fastype_of t_compr)
     fun mk_insert x S =
-      Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S 
+      Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S
     fun mk_set_compr in_insert [] xs =
        rev ((Free ("dots", fastype_of t_compr)) ::  (* FIXME proper name!? *)
         (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
@@ -968,19 +1016,22 @@
             mk_set_compr (t :: in_insert) ts xs
           else
             let
-              val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
+              val uu as (uuN, uuT) =
+                singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
               val set_compr =
-                HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
-                  frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
+                HOLogic.mk_Collect (uuN, uuT,
+                  fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
+                    frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
             in
               mk_set_compr [] ts
-                (set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))  
+                (set_compr ::
+                  (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
             end
         end
   in
-      foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
-        (map (fn ts => HOLogic.mk_tuple 
-          (map (restore_nat_numerals o restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
+    foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
+      (map (fn ts => HOLogic.mk_tuple
+        (map (restore_nat_numerals o restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
   end
 
 fun values_cmd print_modes soln raw_t state =
@@ -991,30 +1042,31 @@
     val ty' = Term.type_of t'
     val ctxt' = Variable.auto_fixes t' ctxt
     val _ = tracing "Printing terms..."
-    val p = Print_Mode.with_modes print_modes (fn () =>
+  in
+    Print_Mode.with_modes print_modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
-  in Pretty.writeln p end;
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ()
+  end |> Pretty.writeln p
 
 
 (* renewing the values command for Prolog queries *)
 
 val opt_print_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "values"}
     "enumerate and print comprehensions"
     (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
      >> (fn ((print_modes, soln), t) => Toplevel.keep
-          (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
+          (values_cmd print_modes soln t))) (*FIXME does not preserve the previous functionality*)
 
 
 (* quickcheck generator *)
 
 (* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
 
-val active = Attrib.setup_config_bool @{binding quickcheck_prolog_active} (K true);
+val active = Attrib.setup_config_bool @{binding quickcheck_prolog_active} (K true)
 
 fun test_term ctxt (t, eval_terms) =
   let
@@ -1035,14 +1087,17 @@
       p (translate_const constant_table full_constname, map (Var o fst) vs') (map fst vs') (SOME 1)
     val _ = tracing "Restoring terms..."
     val counterexample =
-      case tss of
+      (case tss of
         [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
-      | _ => NONE
+      | _ => NONE)
   in
     Quickcheck.Result
-      {counterexample = Option.map (pair true o curry (op ~~) (Term.add_free_names t [])) counterexample,
-       evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
-  end;
+      {counterexample =
+        Option.map (pair true o curry (op ~~) (Term.add_free_names t [])) counterexample,
+       evaluation_terms = Option.map (K []) counterexample,
+       timings = [],
+       reports = []}
+  end
 
 fun test_goals ctxt _ insts goals =
   let
@@ -1050,6 +1105,5 @@
   in
     Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
   end
-  
-  
-end;
+
+end
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -133,14 +133,16 @@
   val merge = Graph.merge eq_pred_data;
 );
 
+
 (* queries *)
 
 fun lookup_pred_data ctxt name =
   Option.map rep_pred_data (try (Graph.get_node (PredData.get (Proof_Context.theory_of ctxt))) name)
 
-fun the_pred_data ctxt name = case lookup_pred_data ctxt name
- of NONE => error ("No such predicate " ^ quote name)  
-  | SOME data => data;
+fun the_pred_data ctxt name =
+  (case lookup_pred_data ctxt name of
+    NONE => error ("No such predicate " ^ quote name)  
+  | SOME data => data)
 
 val is_registered = is_some oo lookup_pred_data
 
@@ -150,24 +152,26 @@
 
 val names_of = map fst o #intros oo the_pred_data
 
-fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
- of NONE => error ("No elimination rule for predicate " ^ quote name)
-  | SOME thm => thm
+fun the_elim_of ctxt name =
+  (case #elim (the_pred_data ctxt name) of
+    NONE => error ("No elimination rule for predicate " ^ quote name)
+  | SOME thm => thm)
   
 val has_elim = is_some o #elim oo the_pred_data
 
 fun function_names_of compilation ctxt name =
-  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
-    NONE => error ("No " ^ string_of_compilation compilation
-      ^ " functions defined for predicate " ^ quote name)
-  | SOME fun_names => fun_names
+  (case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
+    NONE =>
+      error ("No " ^ string_of_compilation compilation ^
+        " functions defined for predicate " ^ quote name)
+  | SOME fun_names => fun_names)
 
 fun function_name_of compilation ctxt name mode =
-  case AList.lookup eq_mode
-    (function_names_of compilation ctxt name) mode of
-    NONE => error ("No " ^ string_of_compilation compilation
-      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
-  | SOME function_name => function_name
+  (case AList.lookup eq_mode (function_names_of compilation ctxt name) mode of
+    NONE =>
+      error ("No " ^ string_of_compilation compilation ^
+        " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
+  | SOME function_name => function_name)
 
 fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
 
@@ -177,9 +181,10 @@
 
 val all_random_modes_of = all_modes_of Random
 
-fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
+fun defined_functions compilation ctxt name =
+  (case lookup_pred_data ctxt name of
     NONE => false
-  | SOME data => AList.defined (op =) (#function_names data) compilation
+  | SOME data => AList.defined (op =) (#function_names data) compilation)
 
 fun needs_random ctxt s m =
   member (op =) (#needs_random (the_pred_data ctxt s)) m
@@ -189,10 +194,11 @@
     (AList.lookup eq_mode (#predfun_data (the_pred_data ctxt name)) mode)
 
 fun the_predfun_data ctxt name mode =
-  case lookup_predfun_data ctxt name mode of
-    NONE => error ("No function defined for mode " ^ string_of_mode mode ^
-      " of predicate " ^ name)
-  | SOME data => data;
+  (case lookup_predfun_data ctxt name mode of
+    NONE =>
+      error ("No function defined for mode " ^ string_of_mode mode ^
+        " of predicate " ^ name)
+  | SOME data => data)
 
 val predfun_definition_of = #definition ooo the_predfun_data
 
@@ -221,7 +227,8 @@
         val case_th =
           rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
         val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems
-        val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
+        val pats =
+          map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
         val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
           OF (replicate nargs @{thm refl})
         val thesis =
@@ -242,6 +249,7 @@
     Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
   end
 
+
 (* updaters *)
 
 (* fetching introduction rules or registering introduction rules *)
@@ -249,7 +257,7 @@
 val no_compilation = ([], ([], []))
 
 fun fetch_pred_data ctxt name =
-  case try (Inductive.the_inductive ctxt) name of
+  (case try (Inductive.the_inductive ctxt) name of
     SOME (info as (_, result)) => 
       let
         fun is_intro_of intro =
@@ -267,7 +275,7 @@
       in
         mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
       end
-  | NONE => error ("No such predicate: " ^ quote name)
+  | NONE => error ("No such predicate: " ^ quote name))
 
 fun add_predfun_data name mode data =
   let
@@ -294,16 +302,19 @@
   let
     val (name, _) = dest_Const (fst (strip_intro_concl thm))
     fun cons_intro gr =
-     case try (Graph.get_node gr) name of
-       SOME _ => Graph.map_node name (map_pred_data
-         (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
-     | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
+      (case try (Graph.get_node gr) name of
+        SOME _ =>
+          Graph.map_node name (map_pred_data
+            (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
+      | NONE =>
+          Graph.new_node
+            (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr)
   in PredData.map cons_intro thy end
 
 fun set_elim thm =
   let
-    val (name, _) = dest_Const (fst 
-      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
+    val (name, _) =
+      dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
   in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
 
 fun register_predicate (constname, intros, elim) thy =
@@ -356,12 +367,14 @@
 
 fun extend' value_of edges_of key (G, visited) =
   let
-    val (G', v) = case try (Graph.get_node G) key of
+    val (G', v) =
+      (case try (Graph.get_node G) key of
         SOME v => (G, v)
-      | NONE => (Graph.new_node (key, value_of key) G, value_of key)
-    val (G'', visited') = fold (extend' value_of edges_of)
-      (subtract (op =) visited (edges_of (key, v)))
-      (G', key :: visited)
+      | NONE => (Graph.new_node (key, value_of key) G, value_of key))
+    val (G'', visited') =
+      fold (extend' value_of edges_of)
+        (subtract (op =) visited (edges_of (key, v)))
+        (G', key :: visited)
   in
     (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
   end;
@@ -391,14 +404,15 @@
       end))))
     thy  
 
+
 (* registration of alternative function names *)
 
 structure Alt_Compilations_Data = Theory_Data
 (
-  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
-  val empty = Symtab.empty;
-  val extend = I;
-  fun merge data : T = Symtab.merge (K true) data;
+  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+  fun merge data : T = Symtab.merge (K true) data
 );
 
 fun alternative_compilation_of_global thy pred_name mode =
@@ -416,19 +430,21 @@
       (List.partition (fn (_, (_, random)) => random) compilations)
     val non_random_dummys = map (rpair "dummy") non_random_modes
     val all_dummys = map (rpair "dummy") modes
-    val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
-      @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
+    val dummy_function_names =
+      map (rpair all_dummys) Predicate_Compile_Aux.random_compilations @
+      map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
     val alt_compilations = map (apsnd fst) compilations
   in
-    PredData.map (Graph.new_node
-      (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
+    PredData.map
+      (Graph.new_node
+        (pred_name,
+          mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
     #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
   end
 
 fun functional_compilation fun_name mode compfuns T =
   let
-    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
-      mode (binder_types T)
+    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
     val bs = map (pair "x") inpTs
     val bounds = map Bound (rev (0 upto (length bs) - 1))
     val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
@@ -443,4 +459,4 @@
     (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
     fun_names)
 
-end;
\ No newline at end of file
+end
\ No newline at end of file
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/mode_inference.ML
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -71,8 +71,10 @@
 fun mode_of (Context m) = m
   | mode_of (Term m) = m
   | mode_of (Mode_App (d1, d2)) =
-    (case mode_of d1 of Fun (m, m') =>
-        (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of: derivation has mismatching modes")
+      (case mode_of d1 of
+        Fun (m, m') =>
+          (if eq_mode (m, mode_of d2) then m'
+           else raise Fail "mode_of: derivation has mismatching modes")
       | _ => raise Fail "mode_of: derivation has a non-functional mode")
   | mode_of (Mode_Pair (d1, d2)) =
     Pair (mode_of d1, mode_of d2)
@@ -109,12 +111,12 @@
     (Syntax.string_of_term ctxt (HOLogic.mk_not t)) ^ "(negative premise)"
   | string_of_prem ctxt (Sidecond t) =
     (Syntax.string_of_term ctxt t) ^ "(sidecondition)"
-  | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
+  | string_of_prem _ _ = raise Fail "string_of_prem: unexpected input"
 
 type mode_analysis_options =
   {use_generators : bool,
-  reorder_premises : bool,
-  infer_pos_and_neg_modes : bool}
+   reorder_premises : bool,
+   infer_pos_and_neg_modes : bool}
 
 (*** check if a type is an equality type (i.e. doesn't contain fun)
   FIXME this is only an approximation ***)
@@ -134,7 +136,7 @@
 
 fun error_of p (_, m) is =
   "  Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
-        p ^ " violates mode " ^ string_of_mode m
+  p ^ " violates mode " ^ string_of_mode m
 
 fun is_all_input mode =
   let
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -24,18 +24,20 @@
 
 fun print_intross options thy msg intross =
   if show_intermediate_results options then
-    tracing (msg ^ 
-      (space_implode "\n" (map 
+    tracing (msg ^
+      (space_implode "\n" (map
         (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
            commas (map (Display.string_of_thm_global thy) intros)) intross)))
   else ()
-      
+
 fun print_specs options thy specs =
   if show_intermediate_results options then
-    map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
-      ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
+    map (fn (c, thms) =>
+      "Constant " ^ c ^ " has specification:\n" ^
+        (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
     |> space_implode "\n" |> tracing
   else ()
+
 fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s))
 
 fun map_specs f specs =
@@ -44,8 +46,12 @@
 fun process_specification options specs thy' =
   let
     val _ = print_step options "Compiling predicates to flat introrules..."
-    val specs = map (apsnd (map
-      (fn th => if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) specs
+    val specs =
+      map
+        (apsnd (map
+          (fn th =>
+            if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th)))
+        specs
     val (intross1, thy'') =
       apfst flat (fold_map (Predicate_Compile_Pred.preprocess options) specs thy')
     val _ = print_intross options thy'' "Flattened introduction rules: " intross1
@@ -53,21 +59,24 @@
     val intross2 =
       if function_flattening options then
         if fail_safe_function_flattening options then
-          case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
+          (case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
             SOME intross => intross
           | NONE =>
             (if show_caught_failures options then tracing "Function replacement failed!" else ();
-            intross1)
+             intross1))
         else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
       else
         intross1
     val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2
-    val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..."
-    val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'')
-    val (new_intross, thy'''')  =
+    val _ = print_step options
+      "Introducing new constants for abstractions at higher-order argument positions..."
+    val (intross3, (new_defs, thy''')) =
+      Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'')
+    val (new_intross, thy'''') =
       if not (null new_defs) then
         let
-          val _ = print_step options "Recursively obtaining introduction rules for new definitions..."
+          val _ =
+            print_step options "Recursively obtaining introduction rules for new definitions..."
         in process_specification options new_defs thy''' end
       else ([], thy''')
   in
@@ -75,9 +84,8 @@
   end
 
 fun preprocess_strong_conn_constnames options gr ts thy =
-  if forall (fn (Const (c, _)) =>
-      Core_Data.is_registered (Proof_Context.init_global thy) c) ts then
-    thy
+  if forall (fn (Const (c, _)) => Core_Data.is_registered (Proof_Context.init_global thy) c) ts
+  then thy
   else
     let
       fun get_specs ts = map_filter (fn t =>
@@ -94,9 +102,9 @@
       val (fun_pred_specs, thy1) =
         (if function_flattening options andalso (not (null funnames)) then
           if fail_safe_function_flattening options then
-            case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of
+            (case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of
               SOME (intross, thy) => (intross, thy)
-            | NONE => ([], thy)
+            | NONE => ([], thy))
           else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy
         else ([], thy))
       val _ = print_specs options thy1 fun_pred_specs
@@ -111,8 +119,9 @@
         map (fn (s, ths) => (overload_const thy2 s, map (Axclass.overload thy2) ths)) intross5
       val intross7 = map_specs (map (expand_tuples thy2)) intross6
       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 _ = (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) =
         if specialise options then
           Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
@@ -129,14 +138,17 @@
 fun preprocess options t thy =
   let
     val _ = print_step options "Fetching definitions from theory..."
-    val gr = cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph"
-          (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
+    val gr =
+      cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph"
+        (fn () =>
+          Predicate_Compile_Data.obtain_specification_graph options thy t
           |> (fn gr => Term_Graph.restrict (member (op =) (Term_Graph.all_succs gr [t])) gr))
     val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
   in
     cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process"
-      (fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
-        (Term_Graph.strong_conn gr) thy))
+      (fn () =>
+        fold_rev (preprocess_strong_conn_constnames options gr)
+          (Term_Graph.strong_conn gr) thy)
   end
 
 datatype proposed_modes = Multiple_Preds of (string * (mode * string option) list) list
@@ -145,14 +157,15 @@
 fun extract_options lthy (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
   let
     fun chk s = member (op =) raw_options s
-    val proposed_modes = case proposed_modes of
-          Single_Pred proposed_modes => [(const, proposed_modes)]
-        | Multiple_Preds proposed_modes => map
-          (apfst (Code.read_const (Proof_Context.theory_of lthy))) proposed_modes
+    val proposed_modes =
+      (case proposed_modes of
+        Single_Pred proposed_modes => [(const, proposed_modes)]
+      | Multiple_Preds proposed_modes =>
+          map (apfst (Code.read_const (Proof_Context.theory_of lthy))) proposed_modes)
   in
     Options {
       expected_modes = Option.map (pair const) expected_modes,
-      proposed_modes = 
+      proposed_modes =
         map (apsnd (map fst)) proposed_modes,
       proposed_names =
         maps (fn (predname, ms) => (map_filter
@@ -190,15 +203,14 @@
       let
         val lthy' = Local_Theory.background_theory (preprocess options t) lthy
         val const =
-          case Predicate_Compile_Fun.pred_of_function (Proof_Context.theory_of lthy') const of
+          (case Predicate_Compile_Fun.pred_of_function (Proof_Context.theory_of lthy') const of
             SOME c => c
-          | NONE => const
+          | NONE => const)
         val _ = print_step options "Starting Predicate Compile Core..."
       in
         Predicate_Compile_Core.code_pred options const lthy'
       end
-    else
-      Predicate_Compile_Core.code_pred_cmd options raw_const lthy
+    else Predicate_Compile_Core.code_pred_cmd options raw_const lthy
   end
 
 val setup = Predicate_Compile_Core.setup
@@ -210,10 +222,11 @@
   (Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output ||
     Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs
 and parse_mode_tuple_expr xs =
-  (parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\<times>") -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
-    xs
+  (parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\<times>") -- parse_mode_tuple_expr >> Pair ||
+    parse_mode_basic_expr) xs
 and parse_mode_expr xs =
-  (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\<Rightarrow>") -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
+  (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\<Rightarrow>") -- parse_mode_expr >> Fun ||
+    parse_mode_tuple_expr) xs
 
 val mode_and_opt_proposal = parse_mode_expr --
   Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
@@ -230,6 +243,7 @@
   Scan.optional (@{keyword "("} |-- Args.$$$ "expected_modes" |-- @{keyword ":"} |--
     Parse.enum "," parse_mode_expr --| @{keyword ")"} >> SOME) NONE
 
+
 (* Parser for options *)
 
 val scan_options =
@@ -243,7 +257,7 @@
   end
 
 val opt_print_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
 
 val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
 
@@ -267,6 +281,7 @@
       ((NONE, false), (Pred, []))
   end
 
+
 (* code_pred command and values command *)
 
 val _ =
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -89,17 +89,17 @@
   val funT_of : compilation_funs -> mode -> typ -> typ
   (* Different compilations *)
   datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
-    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq 
+    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
     | Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
   val negative_compilation_of : compilation -> compilation
   val compilation_for_polarity : bool -> compilation -> compilation
-  val is_depth_limited_compilation : compilation -> bool 
+  val is_depth_limited_compilation : compilation -> bool
   val string_of_compilation : compilation -> string
   val compilation_names : (string * compilation) list
   val non_random_compilations : compilation list
   val random_compilations : compilation list
   (* Different options for compiler *)
-  datatype options = Options of {  
+  datatype options = Options of {
     expected_modes : (string * mode list) option,
     proposed_modes : (string * mode list) list,
     proposed_names : ((string * mode) * string) list,
@@ -161,7 +161,7 @@
   val unify_consts : theory -> term list -> term list -> (term list * term list)
   val mk_casesrule : Proof.context -> term -> thm list -> term
   val preprocess_intro : theory -> thm -> thm
-  
+
   val define_quickcheck_predicate :
     term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory
 end;
@@ -211,7 +211,7 @@
   | mode_ord (Bool, Bool) = EQUAL
   | mode_ord (Pair (m1, m2), Pair (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
   | mode_ord (Fun (m1, m2), Fun (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
- 
+
 fun list_fun_mode [] = Bool
   | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)
 
@@ -227,7 +227,7 @@
 fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode'
   | dest_tuple_mode _ = []
 
-fun all_modes_of_typ' (T as Type ("fun", _)) = 
+fun all_modes_of_typ' (T as Type ("fun", _)) =
   let
     val (S, U) = strip_type T
   in
@@ -237,7 +237,7 @@
     else
       [Input, Output]
   end
-  | all_modes_of_typ' (Type (@{type_name Product_Type.prod}, [T1, T2])) = 
+  | all_modes_of_typ' (Type (@{type_name Product_Type.prod}, [T1, T2])) =
     map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2)
   | all_modes_of_typ' _ = [Input, Output]
 
@@ -258,7 +258,7 @@
 fun all_smodes_of_typ (T as Type ("fun", _)) =
   let
     val (S, U) = strip_type T
-    fun all_smodes (Type (@{type_name Product_Type.prod}, [T1, T2])) = 
+    fun all_smodes (Type (@{type_name Product_Type.prod}, [T1, T2])) =
       map_product (curry Pair) (all_smodes T1) (all_smodes T2)
       | all_smodes _ = [Input, Output]
   in
@@ -291,8 +291,9 @@
 
 fun ho_args_of_typ T ts =
   let
-    fun ho_arg (T as Type("fun", [_,_])) (SOME t) = if body_type T = @{typ bool} then [t] else []
-      | ho_arg (Type("fun", [_,_])) NONE = raise Fail "mode and term do not match"
+    fun ho_arg (T as Type ("fun", [_, _])) (SOME t) =
+          if body_type T = @{typ bool} then [t] else []
+      | ho_arg (Type ("fun", [_, _])) NONE = raise Fail "mode and term do not match"
       | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2]))
          (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
           ho_arg T1 (SOME t1) @ ho_arg T2 (SOME t2)
@@ -306,25 +307,25 @@
 fun ho_argsT_of_typ Ts =
   let
     fun ho_arg (T as Type("fun", [_,_])) = if body_type T = @{typ bool} then [T] else []
-      | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) =
+      | ho_arg (Type (@{type_name "Product_Type.prod"}, [T1, T2])) =
           ho_arg T1 @ ho_arg T2
       | ho_arg _ = []
   in
     maps ho_arg Ts
   end
-  
+
 
 (* temporary function should be replaced by unsplit_input or so? *)
 fun replace_ho_args mode hoargs ts =
   let
     fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs')
       | replace (Pair (m1, m2), Const (@{const_name Pair}, T) $ t1 $ t2) hoargs =
-        let
-          val (t1', hoargs') = replace (m1, t1) hoargs
-          val (t2', hoargs'') = replace (m2, t2) hoargs'
-        in
-          (Const (@{const_name Pair}, T) $ t1' $ t2', hoargs'')
-        end
+          let
+            val (t1', hoargs') = replace (m1, t1) hoargs
+            val (t2', hoargs'') = replace (m2, t2) hoargs'
+          in
+            (Const (@{const_name Pair}, T) $ t1' $ t2', hoargs'')
+          end
       | replace (_, t) hoargs = (t, hoargs)
   in
     fst (fold_map replace (strip_fun_mode mode ~~ ts) hoargs)
@@ -333,7 +334,8 @@
 fun ho_argsT_of mode Ts =
   let
     fun ho_arg (Fun _) T = [T]
-      | ho_arg (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
+      | ho_arg (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+          ho_arg m1 T1 @ ho_arg m2 T2
       | ho_arg _ _ = []
   in
     flat (map2 ho_arg (strip_fun_mode mode) Ts)
@@ -379,28 +381,28 @@
 fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
 
 fun fold_map_aterms_prodT comb f (Type (@{type_name Product_Type.prod}, [T1, T2])) s =
-  let
-    val (x1, s') = fold_map_aterms_prodT comb f T1 s
-    val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
-  in
-    (comb x1 x2, s'')
-  end
-  | fold_map_aterms_prodT comb f T s = f T s
+      let
+        val (x1, s') = fold_map_aterms_prodT comb f T1 s
+        val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
+      in
+        (comb x1 x2, s'')
+      end
+  | fold_map_aterms_prodT _ f T s = f T s
 
 fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
-  comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
+      comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
   | map_filter_prod f t = f t
-  
+
 fun split_modeT mode Ts =
   let
     fun split_arg_mode (Fun _) _ = ([], [])
       | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
-        let
-          val (i1, o1) = split_arg_mode m1 T1
-          val (i2, o2) = split_arg_mode m2 T2
-        in
-          (i1 @ i2, o1 @ o2)
-        end
+          let
+            val (i1, o1) = split_arg_mode m1 T1
+            val (i2, o2) = split_arg_mode m2 T2
+          in
+            (i1 @ i2, o1 @ o2)
+          end
       | split_arg_mode Input T = ([T], [])
       | split_arg_mode Output T = ([], [T])
       | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
@@ -427,7 +429,7 @@
       | ascii_string_of_mode' Bool = "b"
       | ascii_string_of_mode' (Pair (m1, m2)) =
           "P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
-      | ascii_string_of_mode' (Fun (m1, m2)) = 
+      | ascii_string_of_mode' (Fun (m1, m2)) =
           "F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B"
     and ascii_string_of_mode'_Fun (Fun (m1, m2)) =
           ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2)
@@ -438,10 +440,11 @@
       | ascii_string_of_mode'_Pair m = ascii_string_of_mode' m
   in ascii_string_of_mode'_Fun mode' end
 
+
 (* premises *)
 
-datatype indprem = Prem of term | Negprem of term | Sidecond of term
-  | Generator of (string * typ);
+datatype indprem =
+  Prem of term | Negprem of term | Sidecond of term | Generator of (string * typ)
 
 fun dest_indprem (Prem t) = t
   | dest_indprem (Negprem t) = t
@@ -453,25 +456,28 @@
   | map_indprem f (Sidecond t) = Sidecond (f t)
   | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T))))
 
+
 (* general syntactic functions *)
 
 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
-  | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
+  | is_equationlike_term
+      (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
   | is_equationlike_term _ = false
-  
-val is_equationlike = is_equationlike_term o prop_of 
+
+val is_equationlike = is_equationlike_term o prop_of
 
 fun is_pred_equation_term (Const ("==", _) $ u $ v) =
-  (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
+      (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
   | is_pred_equation_term _ = false
-  
-val is_pred_equation = is_pred_equation_term o prop_of 
+
+val is_pred_equation = is_pred_equation_term o prop_of
 
 fun is_intro_term constname t =
-  the_default false (try (fn t => case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
-    Const (c, _) => c = constname
-  | _ => false) t)
-  
+  the_default false (try (fn t =>
+    case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
+      Const (c, _) => c = constname
+    | _ => false) t)
+
 fun is_intro constname t = is_intro_term constname (prop_of t)
 
 fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
@@ -486,14 +492,17 @@
     val cnstrs = flat (maps
       (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
       (Symtab.dest (Datatype.get_all thy)));
-    fun check t = (case strip_comb t of
+    fun check t =
+      (case strip_comb t of
         (Var _, []) => true
       | (Free _, []) => true
-      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
-            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
+      | (Const (s, T), ts) =>
+          (case (AList.lookup (op =) cnstrs s, body_type T) of
+            (SOME (i, Tname), Type (Tname', _)) =>
+              length ts = i andalso Tname = Tname' andalso forall check ts
           | _ => false)
       | _ => false)
-  in check end;
+  in check end
 
 (* returns true if t is an application of an datatype constructor *)
 (* which then consequently would be splitted *)
@@ -512,35 +521,37 @@
   else false
 *)
 
-val is_constr = Code.is_constr o Proof_Context.theory_of;
+val is_constr = Code.is_constr o Proof_Context.theory_of
 
 fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
 
 fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
-  let
-    val (xTs, t') = strip_ex t
-  in
-    ((x, T) :: xTs, t')
-  end
+      let
+        val (xTs, t') = strip_ex t
+      in
+        ((x, T) :: xTs, t')
+      end
   | strip_ex t = ([], t)
 
 fun focus_ex t nctxt =
   let
-    val ((xs, Ts), t') = apfst split_list (strip_ex t) 
+    val ((xs, Ts), t') = apfst split_list (strip_ex t)
     val (xs', nctxt') = fold_map Name.variant xs nctxt;
     val ps' = xs' ~~ Ts;
     val vs = map Free ps';
     val t'' = Term.subst_bounds (rev vs, t');
-  in ((ps', t''), nctxt') end;
+  in ((ps', t''), nctxt') end
 
-val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
-  
+val strip_intro_concl = strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of
+
+
 (* introduction rule combinators *)
 
-fun map_atoms f intro = 
+fun map_atoms f intro =
   let
     val (literals, head) = Logic.strip_horn intro
-    fun appl t = (case t of
+    fun appl t =
+      (case t of
         (@{term Not} $ t') => HOLogic.mk_not (f t')
       | _ => f t)
   in
@@ -551,16 +562,18 @@
 fun fold_atoms f intro s =
   let
     val (literals, _) = Logic.strip_horn intro
-    fun appl t s = (case t of
-      (@{term Not} $ t') => f t' s
+    fun appl t s =
+      (case t of
+        (@{term Not} $ t') => f t' s
       | _ => f t s)
   in fold appl (map HOLogic.dest_Trueprop literals) s end
 
 fun fold_map_atoms f intro s =
   let
     val (literals, head) = Logic.strip_horn intro
-    fun appl t s = (case t of
-      (@{term Not} $ t') => apfst HOLogic.mk_not (f t' s)
+    fun appl t s =
+      (case t of
+        (@{term Not} $ t') => apfst HOLogic.mk_not (f t' s)
       | _ => f t s)
     val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
   in
@@ -588,12 +601,14 @@
     Logic.list_implies (premises, f head)
   end
 
+
 (* combinators to apply a function to all basic parts of nested products *)
 
 fun map_products f (Const (@{const_name Pair}, T) $ t1 $ t2) =
   Const (@{const_name Pair}, T) $ map_products f t1 $ map_products f t2
   | map_products f t = f t
 
+
 (* split theorems of case expressions *)
 
 fun prepare_split_thm ctxt split_thm =
@@ -602,7 +617,8 @@
       @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
 
 fun find_split_thm thy (Const (name, _)) = Option.map #split (Datatype.info_of_case thy name)
-  | find_split_thm thy _ = NONE
+  | find_split_thm _ _ = NONE
+
 
 (* lifting term operations to theorems *)
 
@@ -612,10 +628,11 @@
 (*
 fun equals_conv lhs_cv rhs_cv ct =
   case Thm.term_of ct of
-    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct  
-  | _ => error "equals_conv"  
+    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
+  | _ => error "equals_conv"
 *)
 
+
 (* Different compilations *)
 
 datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
@@ -629,9 +646,9 @@
   | negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq
   | negative_compilation_of Neg_Generator_DSeq = Pos_Generator_DSeq
   | negative_compilation_of Pos_Generator_CPS = Neg_Generator_CPS
-  | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS  
+  | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS
   | negative_compilation_of c = c
-  
+
 fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
   | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
   | compilation_for_polarity _ c = c
@@ -641,7 +658,7 @@
   (c = Pos_Generator_DSeq) orelse (c = Pos_Generator_DSeq)
 
 fun string_of_compilation c =
-  case c of
+  (case c of
     Pred => ""
   | Random => "random"
   | Depth_Limited => "depth limited"
@@ -655,9 +672,10 @@
   | Pos_Generator_DSeq => "pos_generator_dseq"
   | Neg_Generator_DSeq => "neg_generator_dseq"
   | Pos_Generator_CPS => "pos_generator_cps"
-  | Neg_Generator_CPS => "neg_generator_cps"
-  
-val compilation_names = [("pred", Pred),
+  | Neg_Generator_CPS => "neg_generator_cps")
+
+val compilation_names =
+ [("pred", Pred),
   ("random", Random),
   ("depth_limited", Depth_Limited),
   ("depth_limited_random", Depth_Limited_Random),
@@ -675,6 +693,7 @@
   Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq,
   Pos_Generator_CPS, Neg_Generator_CPS]
 
+
 (* datastructures and setup for generic compilation *)
 
 datatype compilation_funs = CompilationFuns of {
@@ -688,7 +707,7 @@
   mk_iterate_upto : typ -> term * term * term -> term,
   mk_not : term -> term,
   mk_map : typ -> typ -> term -> term -> term
-};
+}
 
 fun mk_monadT (CompilationFuns funs) = #mk_monadT funs
 fun dest_monadT (CompilationFuns funs) = #dest_monadT funs
@@ -701,19 +720,22 @@
 fun mk_not (CompilationFuns funs) = #mk_not funs
 fun mk_map (CompilationFuns funs) = #mk_map funs
 
+
 (** function types and names of different compilations **)
 
 fun funT_of compfuns mode T =
   let
     val Ts = binder_types T
-    val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
+    val (inTs, outTs) =
+      split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
   in
     inTs ---> (mk_monadT compfuns (HOLogic.mk_tupleT outTs))
-  end;
+  end
+
 
 (* Different options for compiler *)
 
-datatype options = Options of {  
+datatype options = Options of {
   expected_modes : (string * mode list) option,
   proposed_modes : (string * mode list) list,
   proposed_names : ((string * mode) * string) list,
@@ -735,7 +757,7 @@
   detect_switches : bool,
   smart_depth_limiting : bool,
   compilation : compilation
-};
+}
 
 fun expected_modes (Options opt) = #expected_modes opt
 fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
@@ -798,33 +820,37 @@
 fun print_step options s =
   if show_steps options then tracing s else ()
 
+
 (* simple transformations *)
 
 (** tuple processing **)
 
 fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
-  | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
-    (case HOLogic.strip_tupleT (fastype_of arg) of
-      (_ :: _ :: _) =>
-      let
-        fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
-          (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
-          | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
-            let
-              val thy = Proof_Context.theory_of ctxt
-              val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
-              val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
-              val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
-              val args' = map (Pattern.rewrite_term thy [pat] []) args
-            in
-              rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
-            end
-          | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
-        val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
-          (args, (pats, intro_t, ctxt))
-      in
-        rewrite_args args' (pats, intro_t', ctxt')
-      end
+  | rewrite_args (arg::args) (pats, intro_t, ctxt) =
+      (case HOLogic.strip_tupleT (fastype_of arg) of
+        (_ :: _ :: _) =>
+        let
+          fun rewrite_arg'
+                (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
+                (args, (pats, intro_t, ctxt)) =
+                rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
+            | rewrite_arg'
+                (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
+                let
+                  val thy = Proof_Context.theory_of ctxt
+                  val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
+                  val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
+                  val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
+                  val args' = map (Pattern.rewrite_term thy [pat] []) args
+                in
+                  rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
+                end
+            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
+          val (args', (pats, intro_t', ctxt')) =
+            rewrite_arg' (arg, fastype_of arg) (args, (pats, intro_t, ctxt))
+        in
+          rewrite_args args' (pats, intro_t', ctxt')
+        end
   | _ => rewrite_args args (pats, intro_t, ctxt))
 
 fun rewrite_prem atom =
@@ -834,23 +860,24 @@
 
 fun split_conjuncts_in_assms ctxt th =
   let
-    val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt 
+    val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt
     fun split_conjs i nprems th =
       if i > nprems then th
       else
-        case try Drule.RSN (@{thm conjI}, (i, th)) of
-          SOME th' => split_conjs i (nprems+1) th'
-        | NONE => split_conjs (i+1) nprems th
+        (case try Drule.RSN (@{thm conjI}, (i, th)) of
+          SOME th' => split_conjs i (nprems + 1) th'
+        | NONE => split_conjs (i + 1) nprems th)
   in
-    singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
+    singleton (Variable.export ctxt' ctxt)
+      (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
   end
 
 fun dest_conjunct_prem th =
-  case HOLogic.dest_Trueprop (prop_of th) of
+  (case HOLogic.dest_Trueprop (prop_of th) of
     (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
       dest_conjunct_prem (th RS @{thm conjunct1})
         @ dest_conjunct_prem (th RS @{thm conjunct2})
-    | _ => [th]
+   | _ => [th])
 
 fun expand_tuples thy intro =
   let
@@ -877,6 +904,7 @@
     intro'''''
   end
 
+
 (** making case distributivity rules **)
 (*** this should be part of the datatype package ***)
 
@@ -888,7 +916,7 @@
     val case_combs = Datatype_Prop.make_case_combs case_names descr thy "f";
     fun make comb =
       let
-        val Type ("fun", [T, T']) = fastype_of comb;
+        val Type ("fun", [T, T']) = fastype_of comb
         val (Const (case_name, _), fs) = strip_comb comb
         val used = Term.add_tfree_names comb []
         val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
@@ -952,12 +980,14 @@
       (map (fn th => th RS @{thm eq_reflection}) ths) [] t
   end
 
+
 (*** conversions ***)
 
 fun imp_prems_conv cv ct =
-  case Thm.term_of ct of
+  (case Thm.term_of ct of
     Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
-  | _ => Conv.all_conv ct
+  | _ => Conv.all_conv ct)
+
 
 (** eta contract higher-order arguments **)
 
@@ -968,6 +998,7 @@
     map_term thy (map_concl f o map_atoms f) intro
   end
 
+
 (** remove equalities **)
 
 fun remove_equalities thy intro =
@@ -978,26 +1009,27 @@
         fun remove_eq (prems, concl) =
           let
             fun removable_eq prem =
-              case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of
-                SOME (lhs, rhs) => (case lhs of
-                  Var _ => true
+              (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of
+                SOME (lhs, rhs) =>
+                  (case lhs of
+                    Var _ => true
                   | _ => (case rhs of Var _ => true | _ => false))
-              | NONE => false
+              | NONE => false)
           in
-            case find_first removable_eq prems of
+            (case find_first removable_eq prems of
               NONE => (prems, concl)
             | SOME eq =>
-              let
-                val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
-                val prems' = remove (op =) eq prems
-                val subst = (case lhs of
-                  (v as Var _) =>
-                    (fn t => if t = v then rhs else t)
-                | _ => (case rhs of
-                   (v as Var _) => (fn t => if t = v then lhs else t)))
-              in
-                remove_eq (map (map_aterms subst) prems', map_aterms subst concl)
-              end
+                let
+                  val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+                  val prems' = remove (op =) eq prems
+                  val subst =
+                    (case lhs of
+                      (v as Var _) =>
+                        (fn t => if t = v then rhs else t)
+                    | _ => (case rhs of (v as Var _) => (fn t => if t = v then lhs else t)))
+                in
+                  remove_eq (map (map_aterms subst) prems', map_aterms subst concl)
+                end)
           end
       in
         Logic.list_implies (remove_eq (prems, concl))
@@ -1006,6 +1038,7 @@
     map_term thy remove_eqs intro
   end
 
+
 (* Some last processing *)
 
 fun remove_pointless_clauses intro =
@@ -1013,6 +1046,7 @@
     []
   else [intro]
 
+
 (* some peephole optimisations *)
 
 fun peephole_optimisation thy intro =
@@ -1021,7 +1055,8 @@
     val process =
       rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
     fun process_False intro_t =
-      if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
+      if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"}
+      then NONE else SOME intro_t
     fun process_True intro_t =
       map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
   in
@@ -1033,60 +1068,65 @@
 (* importing introduction rules *)
 
 fun import_intros inp_pred [] ctxt =
-  let
-    val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
-    val T = fastype_of outp_pred
-    val paramTs = ho_argsT_of_typ (binder_types T)
-    val (param_names, _) = Variable.variant_fixes
-      (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
-    val params = map2 (curry Free) param_names paramTs
-  in
-    (((outp_pred, params), []), ctxt')
-  end
+      let
+        val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
+        val T = fastype_of outp_pred
+        val paramTs = ho_argsT_of_typ (binder_types T)
+        val (param_names, _) = Variable.variant_fixes
+          (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
+        val params = map2 (curry Free) param_names paramTs
+      in
+        (((outp_pred, params), []), ctxt')
+      end
   | import_intros inp_pred (th :: ths) ctxt =
-    let
-      val ((_, [th']), ctxt') = Variable.import true [th] ctxt
-      val thy = Proof_Context.theory_of ctxt'
-      val (pred, args) = strip_intro_concl th'
-      val T = fastype_of pred
-      val ho_args = ho_args_of_typ T args
-      fun subst_of (pred', pred) =
-        let
-          val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
-            handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
-            ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
-            ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
-            ^ " in " ^ Display.string_of_thm ctxt th)
-        in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
-      fun instantiate_typ th =
-        let
-          val (pred', _) = strip_intro_concl th
-          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
-            raise Fail "Trying to instantiate another predicate" else ()
-        in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
-      fun instantiate_ho_args th =
-        let
-          val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
-          val ho_args' = map dest_Var (ho_args_of_typ T args')
-        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
-      val outp_pred =
-        Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
-      val ((_, ths'), ctxt1) =
-        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
-    in
-      (((outp_pred, ho_args), th' :: ths'), ctxt1)
-    end
-  
+      let
+        val ((_, [th']), ctxt') = Variable.import true [th] ctxt
+        val thy = Proof_Context.theory_of ctxt'
+        val (pred, args) = strip_intro_concl th'
+        val T = fastype_of pred
+        val ho_args = ho_args_of_typ T args
+        fun subst_of (pred', pred) =
+          let
+            val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
+              handle Type.TYPE_MATCH =>
+                error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
+                  " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred') ^
+                  " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")" ^
+                  " in " ^ Display.string_of_thm ctxt th)
+          in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
+        fun instantiate_typ th =
+          let
+            val (pred', _) = strip_intro_concl th
+            val _ =
+              if not (fst (dest_Const pred) = fst (dest_Const pred')) then
+                raise Fail "Trying to instantiate another predicate"
+              else ()
+          in Thm.certify_instantiate (subst_of (pred', pred), []) th end
+        fun instantiate_ho_args th =
+          let
+            val (_, args') =
+              (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
+            val ho_args' = map dest_Var (ho_args_of_typ T args')
+          in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
+        val outp_pred =
+          Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
+        val ((_, ths'), ctxt1) =
+          Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
+      in
+        (((outp_pred, ho_args), th' :: ths'), ctxt1)
+      end
+
+
 (* generation of case rules from user-given introduction rules *)
 
 fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
-    let
-      val (t1, st') = mk_args2 T1 st
-      val (t2, st'') = mk_args2 T2 st'
-    in
-      (HOLogic.mk_prod (t1, t2), st'')
-    end
-  (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) = 
+      let
+        val (t1, st') = mk_args2 T1 st
+        val (t2, st'') = mk_args2 T2 st'
+      in
+        (HOLogic.mk_prod (t1, t2), st'')
+      end
+  (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) =
     let
       val (S, U) = strip_type T
     in
@@ -1100,11 +1140,11 @@
         end
     end*)
   | mk_args2 T (params, ctxt) =
-    let
-      val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
-    in
-      (Free (x, T), (params, ctxt'))
-    end
+      let
+        val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
+      in
+        (Free (x, T), (params, ctxt'))
+      end
 
 fun mk_casesrule ctxt pred introrules =
   let
@@ -1129,28 +1169,29 @@
     val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
     val cases = map mk_case intros
   in Logic.list_implies (assm :: cases, prop) end;
-  
+
 
 (* unifying constants to have the same type variables *)
 
 fun unify_consts thy cs intr_ts =
-  (let
+  let
      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
      fun varify (t, (i, ts)) =
        let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
-       in (maxidx_of_term t', t'::ts) end;
-     val (i, cs') = List.foldr varify (~1, []) cs;
-     val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
-     val rec_consts = fold add_term_consts_2 cs' [];
-     val intr_consts = fold add_term_consts_2 intr_ts' [];
+       in (maxidx_of_term t', t' :: ts) end
+     val (i, cs') = List.foldr varify (~1, []) cs
+     val (i', intr_ts') = List.foldr varify (i, []) intr_ts
+     val rec_consts = fold add_term_consts_2 cs' []
+     val intr_consts = fold add_term_consts_2 intr_ts' []
      fun unify (cname, cT) =
        let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
-       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
-     val (env, _) = fold unify rec_consts (Vartab.empty, i');
+       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end
+     val (env, _) = fold unify rec_consts (Vartab.empty, i')
      val subst = map_types (Envir.norm_type env)
    in (map subst cs', map subst intr_ts')
-   end) handle Type.TUNIFY =>
-     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
+   end handle Type.TUNIFY =>
+     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts))
+
 
 (* preprocessing rules *)
 
@@ -1163,6 +1204,7 @@
 
 fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
 
+
 (* defining a quickcheck predicate *)
 
 fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
@@ -1171,7 +1213,7 @@
 fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ _ $ B) = strip_imp_concl B
   | strip_imp_concl A = A;
 
-fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+fun strip_horn A = (strip_imp_prems A, strip_imp_concl A)
 
 fun define_quickcheck_predicate t thy =
   let
@@ -1184,9 +1226,10 @@
     val constT = map snd vs' ---> @{typ bool}
     val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
     val const = Const (full_constname, constT)
-    val t = Logic.list_implies
-      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
-       HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
+    val t =
+      Logic.list_implies
+        (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
+          HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
     val intro =
       Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
         (fn _ => ALLGOALS Skip_Proof.cheat_tac)
@@ -1194,4 +1237,4 @@
     ((((full_constname, constT), vs'), intro), thy1)
   end
 
-end;
+end
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -4,30 +4,30 @@
 Structures for different compilations of the predicate compiler.
 *)
 
-structure Predicate_Comp_Funs =
+structure Predicate_Comp_Funs =  (* FIXME proper signature *)
 struct
 
 fun mk_monadT T = Type (@{type_name Predicate.pred}, [T])
 
 fun dest_monadT (Type (@{type_name Predicate.pred}, [T])) = T
-  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
+  | dest_monadT T = raise TYPE ("dest_monadT", [T], [])
 
-fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T);
+fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T)
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end;
+  in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
 
-val mk_plus = HOLogic.mk_binop @{const_name sup};
+val mk_plus = HOLogic.mk_binop @{const_name sup}
 
 fun mk_if cond = Const (@{const_name Predicate.if_pred},
-  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
+  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto T (f, from, to) =
   list_comb (Const (@{const_name Predicate.iterate_upto},
@@ -50,44 +50,48 @@
     val T = dest_monadT (fastype_of f)
   in
     Const (@{const_name Predicate.eval}, mk_monadT T --> T --> HOLogic.boolT) $ f $ x
-  end;
+  end
 
 fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
 
 fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
-  (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp;
+  (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
     mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
-    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-end;
+end
 
-structure CPS_Comp_Funs =
+
+structure CPS_Comp_Funs =  (* FIXME proper signature *)
 struct
 
-fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
+fun mk_monadT T =
+  (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
 
-fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
+fun dest_monadT
+      (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
   | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T)
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end;
+  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
 
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus}
 
 fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
-  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
+  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = error "not implemented yet"
 
@@ -104,14 +108,16 @@
 
 fun mk_map _ _ _ _ = error "not implemented"
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
     mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
-end;
+end
 
-structure Pos_Bounded_CPS_Comp_Funs =
+
+structure Pos_Bounded_CPS_Comp_Funs =  (* FIXME proper signature *)
 struct
 
 val resultT = @{typ "(bool * Code_Evaluation.term list) option"}
@@ -119,13 +125,13 @@
 
 fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "(bool * term list) option"}]),
   @{typ "natural => (bool * term list) option"}])) = T
-  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
+  | dest_monadT T = raise TYPE ("dest_monadT", [T], [])
 
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T)
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end;
+  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
@@ -133,10 +139,11 @@
     Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus}
 
-fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
-  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
+fun mk_if cond =
+  Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
+    HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = error "not implemented yet"
 
@@ -156,14 +163,16 @@
 
 fun mk_map _ _ _ _ = error "not implemented"
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
     mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
-end;
+end
 
-structure Neg_Bounded_CPS_Comp_Funs =
+
+structure Neg_Bounded_CPS_Comp_Funs =  (* FIXME proper signature *)
 struct
 
 fun mk_monadT T =
@@ -171,16 +180,17 @@
     --> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"})
     --> @{typ "natural => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
 
-fun dest_monadT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
-    @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
-    @{typ "natural => term list Quickcheck_Exhaustive.three_valued"}])) = T
+fun dest_monadT
+    (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
+      @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
+      @{typ "natural => term list Quickcheck_Exhaustive.three_valued"}])) = T
   | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T)
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end;
+  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
@@ -188,10 +198,10 @@
     Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus}
 
 fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
-  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
+  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = error "not implemented"
 
@@ -210,7 +220,8 @@
 
 fun mk_map _ _ _ _  = error "not implemented"
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
     mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
@@ -218,7 +229,7 @@
 end;
 
 
-structure RandomPredCompFuns =
+structure RandomPredCompFuns =  (* FIXME proper signature *)
 struct
 
 fun mk_randompredT T =
@@ -226,7 +237,7 @@
 
 fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
   [Type (@{type_name Predicate.pred}, [T]), @{typ Random.seed}])])) = T
-  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
+  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], [])
 
 fun mk_empty T = Const(@{const_name Random_Pred.empty}, mk_randompredT T)
 
@@ -235,7 +246,7 @@
     val T = fastype_of t
   in
     Const (@{const_name Random_Pred.single}, T --> mk_randompredT T) $ t
-  end;
+  end
 
 fun mk_bind (x, f) =
   let
@@ -262,14 +273,16 @@
 fun mk_map T1 T2 tf tp = Const (@{const_name Random_Pred.map},
   (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_randompredT, dest_monadT = dest_randompredT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
 
-end;
+end
 
-structure DSequence_CompFuns =
+
+structure DSequence_CompFuns =  (* FIXME proper signature *)
 struct
 
 fun mk_dseqT T = Type ("fun", [@{typ natural}, Type ("fun", [@{typ bool},
@@ -304,48 +317,51 @@
 fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.map},
   (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_dseqT, dest_monadT = dest_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
 end;
 
-structure New_Pos_DSequence_CompFuns =
+
+structure New_Pos_DSequence_CompFuns =  (* FIXME proper signature *)
 struct
 
 fun mk_pos_dseqT T =
-    @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
+  @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
 
-fun dest_pos_dseqT (Type ("fun", [@{typ natural},
-    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
-  | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
+fun dest_pos_dseqT
+      (Type ("fun", [@{typ natural}, Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
+  | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
+  in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Limited_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
   
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Limited_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
+
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union}
 
-val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union};
-
-fun mk_if cond = Const (@{const_name Limited_Sequence.pos_if_seq},
-  HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
+fun mk_if cond =
+  Const (@{const_name Limited_Sequence.pos_if_seq},
+    HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
@@ -357,56 +373,63 @@
         [Type (@{type_name Option.option}, [@{typ unit}])])
   in Const (@{const_name Limited_Sequence.pos_not_seq}, nT --> pT) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.pos_map},
-  (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
+fun mk_map T1 T2 tf tp =
+  Const (@{const_name Limited_Sequence.pos_map},
+    (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
 
-val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_unlimited_compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-end;
+end
 
-structure New_Neg_DSequence_CompFuns =
+
+structure New_Neg_DSequence_CompFuns =  (* FIXME proper signature *)
 struct
 
 fun mk_neg_dseqT T = @{typ natural} -->
   Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
 
-fun dest_neg_dseqT (Type ("fun", [@{typ natural},
-    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
-  | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
+fun dest_neg_dseqT
+    (Type ("fun", [@{typ natural},
+      Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) =
+      T
+  | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
+  in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Limited_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
   
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Limited_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
+
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union}
 
-val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union};
-
-fun mk_if cond = Const (@{const_name Limited_Sequence.neg_if_seq},
-  HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
+fun mk_if cond =
+  Const (@{const_name Limited_Sequence.neg_if_seq},
+    HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
@@ -418,53 +441,58 @@
         [@{typ unit}])
   in Const (@{const_name Limited_Sequence.neg_not_seq}, pT --> nT) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.neg_map},
-  (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
+fun mk_map T1 T2 tf tp =
+  Const (@{const_name Limited_Sequence.neg_map},
+    (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
 
-val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_unlimited_compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-end;
+end
 
-structure New_Pos_Random_Sequence_CompFuns =
+
+structure New_Pos_Random_Sequence_CompFuns =  (* FIXME proper signature *)
 struct
 
 fun mk_pos_random_dseqT T =
   @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
     @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
 
-fun dest_pos_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
-    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
-    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
-  | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+fun dest_pos_random_dseqT
+    (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
+      Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
+      Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
+  | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, mk_pos_random_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
+  in Const(@{const_name Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
 
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
 
 val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.pos_union};
 
@@ -486,59 +514,66 @@
 
   in Const (@{const_name Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.pos_map},
-  (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
+fun mk_map T1 T2 tf tp =
+  Const (@{const_name Random_Sequence.pos_map},
+    (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
 
-val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_unlimited_compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
+
 end;
 
-structure New_Neg_Random_Sequence_CompFuns =
+
+structure New_Neg_Random_Sequence_CompFuns =  (* FIXME proper signature *)
 struct
 
 fun mk_neg_random_dseqT T =
-   @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
+  @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
     @{typ natural} --> 
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
 
-fun dest_neg_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
-    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
-      Type (@{type_name Lazy_Sequence.lazy_sequence},
-        [Type (@{type_name Option.option}, [T])])])])])])) = T
-  | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+fun dest_neg_random_dseqT
+    (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
+      Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
+        Type (@{type_name Lazy_Sequence.lazy_sequence},
+          [Type (@{type_name Option.option}, [T])])])])])])) = T
+  | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, mk_neg_random_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
+  in Const(@{const_name Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
 
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
+
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union}
 
-val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union};
-
-fun mk_if cond = Const (@{const_name Random_Sequence.neg_if_random_dseq},
-  HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
+fun mk_if cond =
+  Const (@{const_name Random_Sequence.neg_if_random_dseq},
+    HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto T (f, from, to) =
   list_comb (Const (@{const_name Random_Sequence.neg_iterate_upto},
@@ -553,51 +588,58 @@
     @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
   in Const (@{const_name Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.neg_map},
-  (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
+fun mk_map T1 T2 tf tp =
+  Const (@{const_name Random_Sequence.neg_map},
+    (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
 
-val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_unlimited_compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-end;
+end
 
-structure Random_Sequence_CompFuns =
+
+structure Random_Sequence_CompFuns =  (* FIXME proper signature *)
 struct
 
 fun mk_random_dseqT T =
   @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
     HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
 
-fun dest_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
-  Type ("fun", [@{typ Random.seed},
-  Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
-  | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+fun dest_random_dseqT
+    (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
+      Type ("fun", [@{typ Random.seed},
+      Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) =
+      DSequence_CompFuns.dest_dseqT T
+  | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
 
-fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T)
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
+  in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
     Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
-  end;
+  end
+
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union}
 
-val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union};
-
-fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
-  HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
+fun mk_if cond =
+  Const (@{const_name Random_Sequence.if_random_dseq},
+    HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
@@ -609,10 +651,11 @@
 fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
   (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+  Predicate_Compile_Aux.CompilationFuns
     {mk_monadT = mk_random_dseqT, dest_monadT = dest_random_dseqT,
     mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
     mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
 
-end;
+end
 
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -11,15 +11,15 @@
   type options = Predicate_Compile_Aux.options
   type compilation = Predicate_Compile_Aux.compilation
   type compilation_funs = Predicate_Compile_Aux.compilation_funs
-  
+
   val setup : theory -> theory
   val code_pred : options -> string -> Proof.context -> Proof.state
   val code_pred_cmd : options -> string -> Proof.context -> Proof.state
-  val values_cmd : string list -> mode option list option
-    -> ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
+  val values_cmd : string list -> mode option list option ->
+    ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
 
   val values_timeout : real Config.T
-  
+
   val print_stored_rules : Proof.context -> unit
   val print_all_modes : compilation -> Proof.context -> unit
 
@@ -27,19 +27,23 @@
   val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
     Proof.context -> Proof.context
   val put_dseq_result : (unit -> term Limited_Sequence.dseq) -> Proof.context -> Proof.context
-  val put_dseq_random_result : (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term Limited_Sequence.dseq * seed) ->
+  val put_dseq_random_result :
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+      term Limited_Sequence.dseq * seed) ->
     Proof.context -> Proof.context
   val put_new_dseq_result : (unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
   val put_lseq_random_result :
-    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) ->
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
+      term Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
   val put_lseq_random_stats_result :
-    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence) ->
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
+      (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
 
   val code_pred_intro_attrib : attribute
-  (* used by Quickcheck_Generator *) 
+  (* used by Quickcheck_Generator *)
   (* temporary for testing of the compilation *)
   val add_equations : options -> string list -> theory -> theory
   val add_depth_limited_random_equations : options -> string list -> theory -> theory
@@ -54,7 +58,7 @@
   type mode_analysis_options =
    {use_generators : bool,
     reorder_premises : bool,
-    infer_pos_and_neg_modes : bool}  
+    infer_pos_and_neg_modes : bool}
   datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
     | Mode_Pair of mode_derivation * mode_derivation | Term of mode
   val head_mode_of : mode_derivation -> mode
@@ -90,12 +94,14 @@
   Const(@{const_name Code_Evaluation.tracing},
     @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
 
+
 (* representation of inferred clauses with modes *)
 
 type moded_clause = term list * (indprem * mode_derivation) list
 
 type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
 
+
 (* diagnostic display functions *)
 
 fun print_modes options modes =
@@ -152,50 +158,53 @@
 (* validity checks *)
 
 fun check_expected_modes options _ modes =
-  case expected_modes options of
-    SOME (s, ms) => (case AList.lookup (op =) modes s of
-      SOME modes =>
-        let
-          val modes' = map snd modes
-        in
-          if not (eq_set eq_mode (ms, modes')) then
-            error ("expected modes were not inferred:\n"
-            ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
-            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
-          else ()
-        end
-      | NONE => ())
-  | NONE => ()
+  (case expected_modes options of
+    SOME (s, ms) =>
+      (case AList.lookup (op =) modes s of
+        SOME modes =>
+          let
+            val modes' = map snd modes
+          in
+            if not (eq_set eq_mode (ms, modes')) then
+              error ("expected modes were not inferred:\n"
+              ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
+              ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
+            else ()
+          end
+        | NONE => ())
+  | NONE => ())
 
 fun check_proposed_modes options preds modes errors =
-  map (fn (s, _) => case proposed_modes options s of
-    SOME ms => (case AList.lookup (op =) modes s of
-      SOME inferred_ms =>
-        let
-          val preds_without_modes = map fst (filter (null o snd) modes)
-          val modes' = map snd inferred_ms
-        in
-          if not (eq_set eq_mode (ms, modes')) then
-            error ("expected modes were not inferred:\n"
-            ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
-            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
-            ^ (if show_invalid_clauses options then
-            ("For the following clauses, the following modes could not be inferred: " ^ "\n"
-            ^ cat_lines errors) else "") ^
-            (if not (null preds_without_modes) then
-              "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
-            else ""))
-          else ()
-        end
-      | NONE => ())
-  | NONE => ()) preds
+  map (fn (s, _) =>
+    case proposed_modes options s of
+      SOME ms =>
+        (case AList.lookup (op =) modes s of
+          SOME inferred_ms =>
+            let
+              val preds_without_modes = map fst (filter (null o snd) modes)
+              val modes' = map snd inferred_ms
+            in
+              if not (eq_set eq_mode (ms, modes')) then
+                error ("expected modes were not inferred:\n"
+                ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
+                ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
+                ^ (if show_invalid_clauses options then
+                ("For the following clauses, the following modes could not be inferred: " ^ "\n"
+                ^ cat_lines errors) else "") ^
+                (if not (null preds_without_modes) then
+                  "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
+                else ""))
+              else ()
+            end
+        | NONE => ())
+    | NONE => ()) preds
 
 fun check_matches_type ctxt predname T ms =
   let
     fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
       | check m (Type("fun", _)) = (m = Input orelse m = Output)
       | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
-          check m1 T1 andalso check m2 T2 
+          check m1 T1 andalso check m2 T2
       | check Input _ = true
       | check Output _ = true
       | check Bool @{typ bool} = true
@@ -203,30 +212,32 @@
     fun check_consistent_modes ms =
       if forall (fn Fun _ => true | _ => false) ms then
         pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
-        |> (fn (res1, res2) => res1 andalso res2) 
+        |> (fn (res1, res2) => res1 andalso res2)
       else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
         true
       else if forall (fn Bool => true | _ => false) ms then
         true
       else
         false
-    val _ = map
-      (fn mode =>
+    val _ =
+      map (fn mode =>
         if length (strip_fun_mode mode) = length (binder_types T)
           andalso (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then ()
-        else error (string_of_mode mode ^ " is not a valid mode for " ^ Syntax.string_of_typ ctxt T
-        ^ " at predicate " ^ predname)) ms
+        else
+          error (string_of_mode mode ^ " is not a valid mode for " ^
+            Syntax.string_of_typ ctxt T ^ " at predicate " ^ predname)) ms
     val _ =
-     if check_consistent_modes ms then ()
-     else error (commas (map string_of_mode ms) ^
-       " are inconsistent modes for predicate " ^ predname)
+      if check_consistent_modes ms then ()
+      else
+        error (commas (map string_of_mode ms) ^ " are inconsistent modes for predicate " ^ predname)
   in
     ms
   end
 
+
 (* compilation modifiers *)
 
-structure Comp_Mod =
+structure Comp_Mod =  (* FIXME proper signature *)
 struct
 
 datatype comp_modifiers = Comp_Modifiers of
@@ -263,29 +274,29 @@
     additional_arguments = additional_arguments, wrap_compilation = wrap_compilation,
     transform_additional_arguments = transform_additional_arguments})
 
-end;
+end
 
 fun unlimited_compfuns_of true New_Pos_Random_DSeq =
-    New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
+      New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
   | unlimited_compfuns_of false New_Pos_Random_DSeq =
-    New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
+      New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
   | unlimited_compfuns_of true Pos_Generator_DSeq =
-    New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
+      New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
   | unlimited_compfuns_of false Pos_Generator_DSeq =
-    New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
+      New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
   | unlimited_compfuns_of _ c =
-    raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)
+      raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)
 
 fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
-    New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
+      New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
   | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
-    New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
+      New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
   | limited_compfuns_of true Pos_Generator_DSeq =
-    New_Pos_DSequence_CompFuns.depth_limited_compfuns
+      New_Pos_DSequence_CompFuns.depth_limited_compfuns
   | limited_compfuns_of false Pos_Generator_DSeq =
-    New_Neg_DSequence_CompFuns.depth_limited_compfuns
+      New_Neg_DSequence_CompFuns.depth_limited_compfuns
   | limited_compfuns_of _ c =
-    raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)
+      raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)
 
 val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
   {
@@ -328,7 +339,7 @@
   compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn T => fn additional_arguments =>
   list_comb (Const(@{const_name Random_Pred.iter},
-  [@{typ natural}, @{typ natural}, @{typ Random.seed}] ---> 
+  [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
     Predicate_Comp_Funs.mk_monadT T), additional_arguments)),
   modify_funT = (fn T =>
     let
@@ -354,7 +365,7 @@
   compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn T => fn additional_arguments =>
   list_comb (Const(@{const_name Random_Pred.iter},
-  [@{typ natural}, @{typ natural}, @{typ Random.seed}] ---> 
+  [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
     Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)),
   modify_funT = (fn T =>
     let
@@ -505,7 +516,7 @@
    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
-  
+
 val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   {
   compilation = Neg_Generator_DSeq,
@@ -534,7 +545,7 @@
   wrap_compilation = K (K (K (K (K I))))
    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   transform_additional_arguments = K I : (indprem -> term list -> term list)
-  }  
+  }
 
 val neg_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
   {
@@ -548,30 +559,32 @@
    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
-  
+
 fun negative_comp_modifiers_of comp_modifiers =
-    (case Comp_Mod.compilation comp_modifiers of
-      Pos_Random_DSeq => neg_random_dseq_comp_modifiers
-    | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
-    | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
-    | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers 
-    | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
-    | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
-    | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
-    | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
-    | _ => comp_modifiers)
+  (case Comp_Mod.compilation comp_modifiers of
+    Pos_Random_DSeq => neg_random_dseq_comp_modifiers
+  | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
+  | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
+  | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
+  | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
+  | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
+  | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
+  | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
+  | _ => comp_modifiers)
+
 
 (* term construction *)
 
-fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
-      NONE => (Free (s, T), (names, (s, [])::vs))
-    | SOME xs =>
-        let
-          val s' = singleton (Name.variant_list names) s;
-          val v = Free (s', T)
-        in
-          (v, (s'::names, AList.update (op =) (s, v::xs) vs))
-        end);
+fun mk_v (names, vs) s T =
+  (case AList.lookup (op =) vs s of
+    NONE => (Free (s, T), (names, (s, [])::vs))
+  | SOME xs =>
+      let
+        val s' = singleton (Name.variant_list names) s;
+        val v = Free (s', T)
+      in
+        (v, (s'::names, AList.update (op =) (s, v::xs) vs))
+      end);
 
 fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
   | distinct_v (t $ u) nvs =
@@ -587,7 +600,7 @@
   let
     fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
           let
-            val (bs2, i') = mk_bounds T2 i 
+            val (bs2, i') = mk_bounds T2 i
             val (bs1, i'') = mk_bounds T1 i'
           in
             (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
@@ -608,17 +621,17 @@
     fold_rev mk_split_abs (binder_types T) inner_term
   end
 
-fun compile_arg compilation_modifiers _ _ param_modes arg = 
+fun compile_arg compilation_modifiers _ _ param_modes arg =
   let
     fun map_params (t as Free (f, T)) =
-      (case (AList.lookup (op =) param_modes f) of
-          SOME mode =>
-            let
-              val T' = Comp_Mod.funT_of compilation_modifiers mode T
-            in
-              mk_Eval_of (Free (f, T'), T) mode
-            end
-        | NONE => t)
+          (case (AList.lookup (op =) param_modes f) of
+              SOME mode =>
+                let
+                  val T' = Comp_Mod.funT_of compilation_modifiers mode T
+                in
+                  mk_Eval_of (Free (f, T'), T) mode
+                end
+          | NONE => t)
       | map_params t = t
   in
     map_aterms map_params arg
@@ -654,39 +667,40 @@
     val compfuns = Comp_Mod.compfuns compilation_modifiers
     fun expr_of (t, deriv) =
       (case (t, deriv) of
-        (t, Term Input) => SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
+        (t, Term Input) =>
+          SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
       | (_, Term Output) => NONE
       | (Const (name, T), Context mode) =>
-        (case alternative_compilation_of ctxt name mode of
-          SOME alt_comp => SOME (alt_comp compfuns T)
-        | NONE =>
-          SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
-            ctxt name mode,
-            Comp_Mod.funT_of compilation_modifiers mode T)))
+          (case alternative_compilation_of ctxt name mode of
+            SOME alt_comp => SOME (alt_comp compfuns T)
+          | NONE =>
+            SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
+              ctxt name mode,
+              Comp_Mod.funT_of compilation_modifiers mode T)))
       | (Free (s, T), Context m) =>
-        (case (AList.lookup (op =) param_modes s) of
-          SOME _ => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
-        | NONE =>
-        let
-          val bs = map (pair "x") (binder_types (fastype_of t))
-          val bounds = map Bound (rev (0 upto (length bs) - 1))
-        in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
+          (case (AList.lookup (op =) param_modes s) of
+            SOME _ => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+          | NONE =>
+              let
+                val bs = map (pair "x") (binder_types (fastype_of t))
+                val bounds = map Bound (rev (0 upto (length bs) - 1))
+              in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
       | (t, Context _) =>
-        let
-          val bs = map (pair "x") (binder_types (fastype_of t))
-          val bounds = map Bound (rev (0 upto (length bs) - 1))
-        in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
+          let
+            val bs = map (pair "x") (binder_types (fastype_of t))
+            val bounds = map Bound (rev (0 upto (length bs) - 1))
+          in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
       | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
-        (case (expr_of (t1, d1), expr_of (t2, d2)) of
-          (NONE, NONE) => NONE
-        | (NONE, SOME t) => SOME t
-        | (SOME t, NONE) => SOME t
-        | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2)))
+          (case (expr_of (t1, d1), expr_of (t2, d2)) of
+            (NONE, NONE) => NONE
+          | (NONE, SOME t) => SOME t
+          | (SOME t, NONE) => SOME t
+          | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2)))
       | (t1 $ t2, Mode_App (deriv1, deriv2)) =>
-        (case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of
-          (SOME t, NONE) => SOME t
-         | (SOME t, SOME u) => SOME (t $ u)
-         | _ => error "something went wrong here!"))
+          (case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of
+            (SOME t, NONE) => SOME t
+           | (SOME t, SOME u) => SOME (t $ u)
+           | _ => error "something went wrong here!"))
   in
     list_comb (the (expr_of (t, deriv)), additional_arguments)
   end
@@ -721,51 +735,56 @@
             val mode = head_mode_of deriv
             val additional_arguments' =
               Comp_Mod.transform_additional_arguments compilation_modifiers p additional_arguments
-            val (compiled_clause, rest) = case p of
-               Prem t =>
-                 let
-                   val u =
-                     compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments'
-                   val (_, out_ts''') = split_mode mode (snd (strip_comb t))
-                   val rest = compile_prems out_ts''' vs' names'' ps
-                 in
-                   (u, rest)
-                 end
-             | Negprem t =>
-                 let
-                   val neg_compilation_modifiers =
-                     negative_comp_modifiers_of compilation_modifiers
-                   val u = mk_not compfuns
-                     (compile_expr neg_compilation_modifiers ctxt (t, deriv) param_modes additional_arguments')
-                   val (_, out_ts''') = split_mode mode (snd (strip_comb t))
-                   val rest = compile_prems out_ts''' vs' names'' ps
-                 in
-                   (u, rest)
-                 end
-             | Sidecond t =>
-                 let
-                   val t = compile_arg compilation_modifiers additional_arguments
-                     ctxt param_modes t
-                   val rest = compile_prems [] vs' names'' ps;
-                 in
-                   (mk_if compfuns t, rest)
-                 end
-             | Generator (v, T) =>
-                 let
-                   val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
-                   val rest = compile_prems [Free (v, T)]  vs' names'' ps;
-                 in
-                   (u, rest)
-                 end
+            val (compiled_clause, rest) =
+              (case p of
+                Prem t =>
+                  let
+                    val u =
+                      compile_expr compilation_modifiers ctxt (t, deriv)
+                       param_modes additional_arguments'
+                    val (_, out_ts''') = split_mode mode (snd (strip_comb t))
+                    val rest = compile_prems out_ts''' vs' names'' ps
+                  in
+                    (u, rest)
+                  end
+              | Negprem t =>
+                  let
+                    val neg_compilation_modifiers =
+                      negative_comp_modifiers_of compilation_modifiers
+                    val u =
+                     mk_not compfuns
+                       (compile_expr neg_compilation_modifiers ctxt (t, deriv)
+                         param_modes additional_arguments')
+                    val (_, out_ts''') = split_mode mode (snd (strip_comb t))
+                    val rest = compile_prems out_ts''' vs' names'' ps
+                  in
+                    (u, rest)
+                  end
+              | Sidecond t =>
+                  let
+                    val t = compile_arg compilation_modifiers additional_arguments
+                      ctxt param_modes t
+                    val rest = compile_prems [] vs' names'' ps;
+                  in
+                    (mk_if compfuns t, rest)
+                  end
+              | Generator (v, T) =>
+                  let
+                    val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
+                    val rest = compile_prems [Free (v, T)]  vs' names'' ps;
+                  in
+                    (u, rest)
+                  end)
           in
             compile_match constr_vs' eqs out_ts''
               (mk_bind compfuns (compiled_clause, rest))
           end
-    val prem_t = compile_prems in_ts' (map fst param_modes) all_vs' moded_ps;
+    val prem_t = compile_prems in_ts' (map fst param_modes) all_vs' moded_ps
   in
     mk_bind compfuns (mk_single compfuns inp, prem_t)
   end
 
+
 (* switch detection *)
 
 (** argument position of an inductive predicates and the executable functions **)
@@ -776,23 +795,25 @@
   | input_positions_pair Output = []
   | input_positions_pair (Fun _) = []
   | input_positions_pair (Pair (m1, m2)) =
-    map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)
+      map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)
 
-fun input_positions_of_mode mode = flat (map_index
-   (fn (i, Input) => [(i, [])]
-   | (_, Output) => []
-   | (_, Fun _) => []
-   | (i, m as Pair _) => map (pair i) (input_positions_pair m))
-     (Predicate_Compile_Aux.strip_fun_mode mode))
+fun input_positions_of_mode mode =
+  flat
+    (map_index
+      (fn (i, Input) => [(i, [])]
+        | (_, Output) => []
+        | (_, Fun _) => []
+        | (i, m as Pair _) => map (pair i) (input_positions_pair m))
+      (Predicate_Compile_Aux.strip_fun_mode mode))
 
 fun argument_position_pair _ [] = []
   | argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
   | argument_position_pair (Pair (m1, m2)) (i :: is) =
-    (if eq_mode (m1, Output) andalso i = 2 then
-      argument_position_pair m2 is
-    else if eq_mode (m2, Output) andalso i = 1 then
-      argument_position_pair m1 is
-    else (i :: argument_position_pair (if i = 1 then m1 else m2) is))
+      (if eq_mode (m1, Output) andalso i = 2 then
+        argument_position_pair m2 is
+      else if eq_mode (m2, Output) andalso i = 1 then
+        argument_position_pair m1 is
+      else (i :: argument_position_pair (if i = 1 then m1 else m2) is))
 
 fun argument_position_of mode (i, is) =
   (i - (length (filter (fn Output => true | Fun _ => true | _ => false)
@@ -804,6 +825,7 @@
   | nth_pair (2 :: is) (Const (@{const_name Pair}, _) $ _ $ t2) = nth_pair is t2
   | nth_pair _ _ = raise Fail "unexpected input for nth_tuple"
 
+
 (** switch detection analysis **)
 
 fun find_switch_test ctxt (i, is) (ts, _) =
@@ -811,25 +833,25 @@
     val t = nth_pair is (nth ts i)
     val T = fastype_of t
   in
-    case T of
+    (case T of
       TFree _ => NONE
     | Type (Tcon, _) =>
-      (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of
-        NONE => NONE
-      | SOME cs =>
-        (case strip_comb t of
-          (Var _, []) => NONE
-        | (Free _, []) => NONE
-        | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE))
+        (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of
+          NONE => NONE
+        | SOME cs =>
+            (case strip_comb t of
+              (Var _, []) => NONE
+            | (Free _, []) => NONE
+            | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE)))
   end
 
 fun partition_clause ctxt pos moded_clauses =
   let
     fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
     fun find_switch_test' moded_clause (cases, left) =
-      case find_switch_test ctxt pos moded_clause of
+      (case find_switch_test ctxt pos moded_clause of
         SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
-      | NONE => (cases, moded_clause :: left)
+      | NONE => (cases, moded_clause :: left))
   in
     fold find_switch_test' moded_clauses ([], [])
   end
@@ -845,34 +867,36 @@
         val partition = partition_clause ctxt input_position moded_clauses
         val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
       in
-        case ord (switch, best_switch) of LESS => best_switch
-          | EQUAL => best_switch | GREATER => switch
+        (case ord (switch, best_switch) of
+          LESS => best_switch
+        | EQUAL => best_switch
+        | GREATER => switch)
       end
     fun detect_switches moded_clauses =
-      case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
+      (case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
         SOME (best_pos, (switched_on, left_clauses)) =>
           Node ((best_pos, map (apsnd detect_switches) switched_on),
             detect_switches left_clauses)
-      | NONE => Atom moded_clauses
+      | NONE => Atom moded_clauses)
   in
     detect_switches moded_clauses
   end
 
+
 (** compilation of detected switches **)
 
 fun destruct_constructor_pattern (pat, obj) =
   (case strip_comb pat of
-    (Free _, []) => cons (pat, obj)
+      (Free _, []) => cons (pat, obj)
   | (Const (c, T), pat_args) =>
-    (case strip_comb obj of
-      (Const (c', T'), obj_args) =>
-        (if c = c' andalso T = T' then
-          fold destruct_constructor_pattern (pat_args ~~ obj_args)
-        else raise Fail "pattern and object mismatch")
-    | _ => raise Fail "unexpected object")
+      (case strip_comb obj of
+        (Const (c', T'), obj_args) =>
+          (if c = c' andalso T = T' then
+            fold destruct_constructor_pattern (pat_args ~~ obj_args)
+          else raise Fail "pattern and object mismatch")
+      | _ => raise Fail "unexpected object")
   | _ => raise Fail "unexpected pattern")
 
-
 fun compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
   in_ts' outTs switch_tree =
   let
@@ -920,48 +944,55 @@
           ((map compile_single_case switched_clauses) @
             [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
       in
-        case compile_switch_tree all_vs ctxt_eqs left_clauses of
+        (case compile_switch_tree all_vs ctxt_eqs left_clauses of
           NONE => SOME switch
-        | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp))
+        | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp)))
       end
   in
     compile_switch_tree all_vs [] switch_tree
   end
 
+
 (* compilation of predicates *)
 
 fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
   let
-    val is_terminating = false (* FIXME: requires an termination analysis *)  
+    val is_terminating = false (* FIXME: requires an termination analysis *)
     val compilation_modifiers =
       (if pol then compilation_modifiers else
         negative_comp_modifiers_of compilation_modifiers)
       |> (if is_depth_limited_compilation (Comp_Mod.compilation compilation_modifiers) then
            (if is_terminating then
-             (Comp_Mod.set_compfuns (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
-           else
-             (Comp_Mod.set_compfuns (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
-         else I)
-    val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
-      (all_vs @ param_vs)
+              (Comp_Mod.set_compfuns
+                (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
+            else
+              (Comp_Mod.set_compfuns
+                (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
+          else I)
+    val additional_arguments =
+      Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs)
     val compfuns = Comp_Mod.compfuns compilation_modifiers
     fun is_param_type (T as Type ("fun",[_ , T'])) =
-      is_some (try (dest_monadT compfuns) T) orelse is_param_type T'
+          is_some (try (dest_monadT compfuns) T) orelse is_param_type T'
       | is_param_type T = is_some (try (dest_monadT compfuns) T)
-    val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
-      (binder_types T)
+    val (inpTs, outTs) =
+      split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
+        (binder_types T)
     val funT = Comp_Mod.funT_of compilation_modifiers mode T
-    val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
-      (fn T => fn (param_vs, names) =>
-        if is_param_type T then
-          (Free (hd param_vs, T), (tl param_vs, names))
-        else
-          let
-            val new = singleton (Name.variant_list names) "x"
-          in (Free (new, T), (param_vs, new :: names)) end)) inpTs
+    val (in_ts, _) =
+      fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
+        (fn T => fn (param_vs, names) =>
+          if is_param_type T then
+            (Free (hd param_vs, T), (tl param_vs, names))
+          else
+            let
+              val new = singleton (Name.variant_list names) "x"
+            in (Free (new, T), (param_vs, new :: names)) end)) inpTs
         (param_vs, (all_vs @ param_vs))
-    val in_ts' = map_filter (map_filter_prod
-      (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
+    val in_ts' =
+      map_filter (map_filter_prod
+        (fn t as Free (x, _) =>
+          if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
     val param_modes = param_vs ~~ ho_arg_modes_of mode
     val compilation =
       if detect_switches options then
@@ -971,9 +1002,9 @@
       else
         let
           val cl_ts =
-            map (fn (ts, moded_prems) => 
+            map (fn (ts, moded_prems) =>
               compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
-                (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls;
+                (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls
         in
           Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
             (if null cl_ts then
@@ -982,12 +1013,12 @@
               foldr1 (mk_plus compfuns) cl_ts)
         end
     val fun_const =
-      Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
-      ctxt s mode, funT)
+      Const (function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT)
   in
     HOLogic.mk_Trueprop
       (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
-  end;
+  end
+
 
 (* Definition of executable functions and their intro and elim rules *)
 
@@ -996,36 +1027,36 @@
   | strip_split_abs t = t
 
 fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
-    if eq_mode (m, Input) orelse eq_mode (m, Output) then
+      if eq_mode (m, Input) orelse eq_mode (m, Output) then
+        let
+          val x = singleton (Name.variant_list names) "x"
+        in
+          (Free (x, T), x :: names)
+        end
+      else
+        let
+          val (t1, names') = mk_args is_eval (m1, T1) names
+          val (t2, names'') = mk_args is_eval (m2, T2) names'
+        in
+          (HOLogic.mk_prod (t1, t2), names'')
+        end
+  | mk_args is_eval ((m as Fun _), T) names =
+      let
+        val funT = funT_of Predicate_Comp_Funs.compfuns m T
+        val x = singleton (Name.variant_list names) "x"
+        val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
+        val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
+        val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
+          (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
+      in
+        (if is_eval then t else Free (x, funT), x :: names)
+      end
+  | mk_args _ (_, T) names =
       let
         val x = singleton (Name.variant_list names) "x"
       in
         (Free (x, T), x :: names)
       end
-    else
-      let
-        val (t1, names') = mk_args is_eval (m1, T1) names
-        val (t2, names'') = mk_args is_eval (m2, T2) names'
-      in
-        (HOLogic.mk_prod (t1, t2), names'')
-      end
-  | mk_args is_eval ((m as Fun _), T) names =
-    let
-      val funT = funT_of Predicate_Comp_Funs.compfuns m T
-      val x = singleton (Name.variant_list names) "x"
-      val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
-      val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
-      val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
-        (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
-    in
-      (if is_eval then t else Free (x, funT), x :: names)
-    end
-  | mk_args is_eval (_, T) names =
-    let
-      val x = singleton (Name.variant_list names) "x"
-    in
-      (Free (x, T), x :: names)
-    end
 
 fun create_intro_elim_rule ctxt mode defthm mode_id funT pred =
   let
@@ -1052,8 +1083,9 @@
     val funpropI = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
                      HOLogic.mk_tuple outargs))
     val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
-    val simprules = [defthm, @{thm eval_pred},
-      @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
+    val simprules =
+      [defthm, @{thm eval_pred},
+        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
     val unfolddef_tac =
       Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1
     val introthm = Goal.prove ctxt
@@ -1082,14 +1114,13 @@
     ((introthm, elimthm), opt_neg_introthm)
   end
 
-fun create_constname_of_mode options thy prefix name _ mode = 
+fun create_constname_of_mode options thy prefix name _ mode =
   let
-    val system_proposal = prefix ^ (Long_Name.base_name name)
-      ^ "_" ^ ascii_string_of_mode mode
+    val system_proposal = prefix ^ (Long_Name.base_name name) ^ "_" ^ ascii_string_of_mode mode
     val name = the_default system_proposal (proposed_names options name mode)
   in
     Sign.full_bname thy name
-  end;
+  end
 
 fun create_definitions options preds (name, modes) thy =
   let
@@ -1181,13 +1212,14 @@
 fun dest_prem ctxt params t =
   (case strip_comb t of
     (v as Free _, _) => if member (op =) params v then Prem t else Sidecond t
-  | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem ctxt params t of
-      Prem t => Negprem t
-    | Negprem _ => error ("Double negation not allowed in premise: " ^
-        Syntax.string_of_term ctxt (c $ t)) 
-    | Sidecond t => Sidecond (c $ t))
+  | (c as Const (@{const_name Not}, _), [t]) =>
+      (case dest_prem ctxt params t of
+        Prem t => Negprem t
+      | Negprem _ => error ("Double negation not allowed in premise: " ^
+          Syntax.string_of_term ctxt (c $ t))
+      | Sidecond t => Sidecond (c $ t))
   | (Const (s, _), _) =>
-    if is_registered ctxt s then Prem t else Sidecond t
+      if is_registered ctxt s then Prem t else Sidecond t
   | _ => Sidecond t)
 
 fun prepare_intrs options ctxt prednames intros =
@@ -1204,13 +1236,14 @@
         all_smodes_of_typ T
       else
         all_modes_of_typ T
-    val all_modes = 
+    val all_modes =
       map (fn (s, T) =>
-        (s, case proposed_modes options s of
+        (s,
+          (case proposed_modes options s of
             SOME ms => check_matches_type ctxt s T ms
-          | NONE => generate_modes s T)) preds
+          | NONE => generate_modes s T))) preds
     val params =
-      case intrs of
+      (case intrs of
         [] =>
           let
             val T = snd (hd preds)
@@ -1223,25 +1256,28 @@
             map2 (curry Free) param_names paramTs
           end
       | (intr :: _) =>
-        let
-          val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
-          val one_mode = hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))
-        in
-          ho_args_of one_mode args
-        end
+          let
+            val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
+            val one_mode = hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))
+          in
+            ho_args_of one_mode args
+          end)
     val param_vs = map (fst o dest_Free) params
     fun add_clause intr clauses =
       let
-        val (Const (name, _), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
-        val prems = map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
+        val (Const (name, _), ts) =
+          strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
+        val prems =
+          map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
       in
-        AList.update op = (name, these (AList.lookup op = clauses name) @
-          [(ts, prems)]) clauses
+        AList.update op =
+          (name, these (AList.lookup op = clauses name) @ [(ts, prems)])
+          clauses
       end;
     val clauses = fold add_clause intrs []
   in
     (preds, all_vs, param_vs, all_modes, clauses)
-  end;
+  end
 
 (* sanity check of introduction rules *)
 (* TODO: rethink check with new modes *)
@@ -1258,7 +1294,7 @@
         else
           error ("Format of introduction rule is invalid: tuples must be expanded:"
           ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
-          (Display.string_of_thm_global thy intro)) 
+          (Display.string_of_thm_global thy intro))
       | _ => true
     val prems = Logic.strip_imp_prems (prop_of intro)
     fun check_prem (Prem t) = forall check_arg args
@@ -1288,6 +1324,7 @@
   in forall check prednames end
 *)
 
+
 (* create code equation *)
 
 fun add_code_equations ctxt preds result_thmss =
@@ -1321,6 +1358,7 @@
     map2 add_code_equation preds result_thmss
   end
 
+
 (** main function of predicate compiler **)
 
 datatype steps = Steps of
@@ -1340,11 +1378,12 @@
     fun dest_steps (Steps s) = s
     val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
     val ctxt = Proof_Context.init_global thy
-    val _ = print_step options
-      ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation
-        ^ ") for predicates " ^ commas prednames ^ "...")
-      (*val _ = check_intros_elim_match thy prednames*)
-      (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
+    val _ =
+      print_step options
+        ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation ^
+          ") for predicates " ^ commas prednames ^ "...")
+    (*val _ = check_intros_elim_match thy prednames*)
+    (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
     val _ =
       if show_intermediate_results options then
         tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames)))
@@ -1391,7 +1430,7 @@
   in
     thy'''
   end
-  
+
 fun gen_add_equations steps options names thy =
   let
     fun dest_steps (Steps s) = s
@@ -1498,14 +1537,17 @@
   (Steps {
   define_functions =
     fn options => fn preds => fn (s, modes) =>
-    let
-      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
-      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
-    in define_functions new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
-      options preds (s, pos_modes)
-      #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
-      options preds (s, neg_modes)
-    end,
+      let
+        val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+        val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+      in
+        define_functions new_pos_random_dseq_comp_modifiers
+          New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
+          options preds (s, pos_modes) #>
+        define_functions new_neg_random_dseq_comp_modifiers
+          New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
+          options preds (s, neg_modes)
+      end,
   prove = prove_by_skip,
   add_code_equations = K (K I),
   comp_modifiers = new_pos_random_dseq_comp_modifiers,
@@ -1515,16 +1557,16 @@
 val add_generator_dseq_equations = gen_add_equations
   (Steps {
   define_functions =
-  fn options => fn preds => fn (s, modes) =>
-    let
-      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
-      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
-    in 
-      define_functions pos_generator_dseq_comp_modifiers New_Pos_DSequence_CompFuns.depth_limited_compfuns
-        options preds (s, pos_modes)
-      #> define_functions neg_generator_dseq_comp_modifiers New_Neg_DSequence_CompFuns.depth_limited_compfuns
-        options preds (s, neg_modes)
-    end,
+    fn options => fn preds => fn (s, modes) =>
+      let
+        val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+        val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+      in
+        define_functions pos_generator_dseq_comp_modifiers
+          New_Pos_DSequence_CompFuns.depth_limited_compfuns options preds (s, pos_modes) #>
+        define_functions neg_generator_dseq_comp_modifiers
+          New_Neg_DSequence_CompFuns.depth_limited_compfuns options preds (s, neg_modes)
+      end,
   prove = prove_by_skip,
   add_code_equations = K (K I),
   comp_modifiers = pos_generator_dseq_comp_modifiers,
@@ -1534,23 +1576,23 @@
 val add_generator_cps_equations = gen_add_equations
   (Steps {
   define_functions =
-  fn options => fn preds => fn (s, modes) =>
-    let
-      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
-      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
-    in 
-      define_functions pos_generator_cps_comp_modifiers Pos_Bounded_CPS_Comp_Funs.compfuns
-        options preds (s, pos_modes)
-      #> define_functions neg_generator_cps_comp_modifiers Neg_Bounded_CPS_Comp_Funs.compfuns
-        options preds (s, neg_modes)
-    end,
+    fn options => fn preds => fn (s, modes) =>
+      let
+        val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+        val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+      in
+        define_functions pos_generator_cps_comp_modifiers Pos_Bounded_CPS_Comp_Funs.compfuns
+          options preds (s, pos_modes)
+        #> define_functions neg_generator_cps_comp_modifiers Neg_Bounded_CPS_Comp_Funs.compfuns
+          options preds (s, neg_modes)
+      end,
   prove = prove_by_skip,
   add_code_equations = K (K I),
   comp_modifiers = pos_generator_cps_comp_modifiers,
   use_generators = true,
   qname = "generator_cps_equation"})
-  
-  
+
+
 (** user interface **)
 
 (* code_pred_intro attribute *)
@@ -1568,9 +1610,11 @@
 
 val default_values_timeout = if ML_System.is_smlnj then 1200.0 else 40.0
 
-val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
+val values_timeout =
+  Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
 
-val setup = PredData.put (Graph.empty) #>
+val setup =
+  PredData.put (Graph.empty) #>
   Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
     "adding alternative introduction rules for code generation of inductive predicates"
 
@@ -1592,7 +1636,7 @@
         val T = Sign.the_const_type thy' const
         val pred = Const (const, T)
         val intros = intros_of ctxt' const
-      in mk_casesrule lthy' pred intros end  
+      in mk_casesrule lthy' pred intros end
     val cases_rules = map mk_cases preds
     val cases =
       map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
@@ -1633,6 +1677,7 @@
 val code_pred = generic_code_pred (K I);
 val code_pred_cmd = generic_code_pred Code.read_const
 
+
 (* transformation for code generation *)
 
 (* FIXME just one data slot (record) per program unit *)
@@ -1695,13 +1740,16 @@
 
 fun dest_special_compr t =
   let
-    val (inner_t, T_compr) = case t of (Const (@{const_name Collect}, _) $ Abs (_, T, t)) => (t, T)
-      | _ => raise TERM ("dest_special_compr", [t])
+    val (inner_t, T_compr) =
+      (case t of
+        (Const (@{const_name Collect}, _) $ Abs (_, T, t)) => (t, T)
+      | _ => raise TERM ("dest_special_compr", [t]))
     val (Ts, conj) = apfst (map snd) (Predicate_Compile_Aux.strip_ex inner_t)
     val [eq, body] = HOLogic.dest_conj conj
-    val rhs = case HOLogic.dest_eq eq of
+    val rhs =
+      (case HOLogic.dest_eq eq of
         (Bound i, rhs) => if i = length Ts then rhs else raise TERM ("dest_special_compr", [t])
-      | _ => raise TERM ("dest_special_compr", [t])
+      | _ => raise TERM ("dest_special_compr", [t]))
     val output_names = Name.variant_list (fold Term.add_free_names [rhs, body] [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
     val output_frees = map2 (curry Free) output_names (rev Ts)
@@ -1712,9 +1760,11 @@
   end
 
 fun dest_general_compr ctxt t_compr =
-  let      
-    val inner_t = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
-      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);    
+  let
+    val inner_t =
+      (case t_compr of
+        (Const (@{const_name Collect}, _) $ t) => t
+      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
     val (body, Ts, fp) = HOLogic.strip_psplits inner_t;
     val output_names = Name.variant_list (Term.add_free_names body [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
@@ -1733,24 +1783,28 @@
     val compfuns = Comp_Mod.compfuns comp_modifiers
     val all_modes_of = all_modes_of compilation
     val (((body, output), T_compr), output_names) =
-      case try dest_special_compr t_compr of SOME r => r | NONE => dest_general_compr ctxt t_compr
+      (case try dest_special_compr t_compr of
+        SOME r => r
+      | NONE => dest_general_compr ctxt t_compr)
     val (Const (name, _), all_args) =
-      case strip_comb body of
+      (case strip_comb body of
         (Const (name, T), all_args) => (Const (name, T), all_args)
-      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
+      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head))
   in
     if defined_functions compilation ctxt name then
       let
-        fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
-          | extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input
+        fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) =
+              Pair (extract_mode t1, extract_mode t2)
+          | extract_mode (Free (x, _)) =
+              if member (op =) output_names x then Output else Input
           | extract_mode _ = Input
         val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool
         fun valid modes1 modes2 =
-          case int_ord (length modes1, length modes2) of
+          (case int_ord (length modes1, length modes2) of
             GREATER => error "Not enough mode annotations"
           | LESS => error "Too many mode annotations"
-          | EQUAL => forall (fn (_, NONE) => true | (m, SOME m2) => eq_mode (m, m2))
-            (modes1 ~~ modes2)
+          | EQUAL =>
+              forall (fn (_, NONE) => true | (m, SOME m2) => eq_mode (m, m2)) (modes1 ~~ modes2))
         fun mode_instance_of (m1, m2) =
           let
             fun instance_of (Fun _, Input) = true
@@ -1778,12 +1832,14 @@
               the_default true (Option.map (valid modes) param_user_modes)
             end)
           |> map fst
-        val deriv = case derivs of
-            [] => error ("No mode possible for comprehension "
-                    ^ Syntax.string_of_term ctxt t_compr)
+        val deriv =
+          (case derivs of
+            [] =>
+              error ("No mode possible for comprehension " ^ Syntax.string_of_term ctxt t_compr)
           | [d] => d
-          | d :: _ :: _ => (warning ("Multiple modes possible for comprehension "
-                    ^ Syntax.string_of_term ctxt t_compr); d);
+          | d :: _ :: _ =>
+              (warning ("Multiple modes possible for comprehension " ^
+                Syntax.string_of_term ctxt t_compr); d))
         val (_, outargs) = split_mode (head_mode_of deriv) all_args
         val t_pred = compile_expr comp_modifiers ctxt
           (body, deriv) [] additional_arguments;
@@ -1805,32 +1861,35 @@
       in count' 0 xs end
     fun accumulate xs = (map (fn x => (x, count xs x)) o sort int_ord o distinct (op =)) xs;
     val comp_modifiers =
-      case compilation of
-          Pred => predicate_comp_modifiers
-        | Random => random_comp_modifiers
-        | Depth_Limited => depth_limited_comp_modifiers
-        | Depth_Limited_Random => depth_limited_random_comp_modifiers
-        (*| Annotated => annotated_comp_modifiers*)
-        | DSeq => dseq_comp_modifiers
-        | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
-        | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
-        | Pos_Generator_DSeq => pos_generator_dseq_comp_modifiers
+      (case compilation of
+        Pred => predicate_comp_modifiers
+      | Random => random_comp_modifiers
+      | Depth_Limited => depth_limited_comp_modifiers
+      | Depth_Limited_Random => depth_limited_random_comp_modifiers
+      (*| Annotated => annotated_comp_modifiers*)
+      | DSeq => dseq_comp_modifiers
+      | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
+      | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
+      | Pos_Generator_DSeq => pos_generator_dseq_comp_modifiers)
     val compfuns = Comp_Mod.compfuns comp_modifiers
     val additional_arguments =
-      case compilation of
+      (case compilation of
         Pred => []
-      | Random => map (HOLogic.mk_number @{typ "natural"}) arguments @
-        [@{term "(1, 1) :: natural * natural"}]
+      | Random =>
+          map (HOLogic.mk_number @{typ "natural"}) arguments @
+            [@{term "(1, 1) :: natural * natural"}]
       | Annotated => []
       | Depth_Limited => [HOLogic.mk_number @{typ "natural"} (hd arguments)]
-      | Depth_Limited_Random => map (HOLogic.mk_number @{typ "natural"}) arguments @
-        [@{term "(1, 1) :: natural * natural"}]
+      | Depth_Limited_Random =>
+          map (HOLogic.mk_number @{typ "natural"}) arguments @
+            [@{term "(1, 1) :: natural * natural"}]
       | DSeq => []
       | Pos_Random_DSeq => []
       | New_Pos_Random_DSeq => []
-      | Pos_Generator_DSeq => []
-    val t = analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr;
-    val T = dest_monadT compfuns (fastype_of t);
+      | Pos_Generator_DSeq => [])
+    val t =
+      analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr
+    val T = dest_monadT compfuns (fastype_of t)
     val t' =
       if stats andalso compilation = New_Pos_Random_DSeq then
         mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ natural}))
@@ -1890,7 +1949,7 @@
               (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
-                  thy NONE 
+                  thy NONE
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.map proc)
                     t' [] nrandom size seed depth))) ())
@@ -1908,20 +1967,21 @@
     val setT = HOLogic.mk_setT T
     val elems = HOLogic.mk_set T ts
     val ([dots], ctxt') =
-      Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt 
+      Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt
     (* check expected values *)
     val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
     val () =
-      case raw_expected of
+      (case raw_expected of
         NONE => ()
       | SOME s =>
         if eq_set (op =) (HOLogic.dest_set (Syntax.read_term ctxt s), ts) then ()
         else
           error ("expected and computed values do not match:\n" ^
             "expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^
-            "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
+            "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n"))
   in
-    ((if k = ~1 orelse length ts < k then elems else union $ elems $ Free (dots, setT), statistics), ctxt')
+    ((if k = ~1 orelse length ts < k then elems else union $ elems $ Free (dots, setT), statistics),
+      ctxt')
   end;
 
 fun values_cmd print_modes param_user_modes options k raw_t state =
@@ -1932,9 +1992,9 @@
     val ty' = Term.type_of t'
     val ctxt'' = Variable.auto_fixes t' ctxt'
     val pretty_stat =
-      case stats of
-          NONE => []
-        | SOME xs =>
+      (case stats of
+        NONE => []
+      | SOME xs =>
           let
             val total = fold (curry (op +)) (map snd xs) 0
             fun pretty_entry (s, n) =
@@ -1943,13 +2003,14 @@
                Pretty.str (string_of_int n), Pretty.fbrk]
           in
             [Pretty.fbrk, Pretty.str "Statistics:", Pretty.fbrk,
-             Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
-             @ maps pretty_entry xs
-          end
-    val p = Print_Mode.with_modes print_modes (fn () =>
+             Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk] @
+              maps pretty_entry xs
+          end)
+  in
+    Print_Mode.with_modes print_modes (fn () =>
       Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt'' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt'' ty')]
-        @ pretty_stat)) ();
-  in Pretty.writeln p end;
+        @ pretty_stat)) ()
+  end |> Pretty.writeln
 
-end;
+end
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -11,11 +11,11 @@
   val keep_function : theory -> string -> bool
   val processed_specs : theory -> string -> (string * thm list) list option
   val store_processed_specs : (string * (string * thm list) list) -> theory -> theory
-  
+
   val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list
   val obtain_specification_graph :
     Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
-    
+
   val present_graph : thm list Term_Graph.T -> unit
   val normalize_equation : theory -> thm -> thm
 end;
@@ -66,7 +66,7 @@
   let
     val _ $ u = Logic.strip_imp_concl t
   in fst (strip_comb u) end
-(*  
+(*
   in case pred of
     Const (c, T) => c
     | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
@@ -75,9 +75,9 @@
 val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
 
 fun defining_const_of_introrule th =
-  case defining_term_of_introrule th
-   of Const (c, _) => c
-    | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
+  (case defining_term_of_introrule th of
+    Const (c, _) => c
+  | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th]))
 
 (*TODO*)
 fun is_introlike_term _ = true
@@ -85,29 +85,29 @@
 val is_introlike = is_introlike_term o prop_of
 
 fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
-  (case strip_comb u of
-    (Const (_, T), args) =>
-      if (length (binder_types T) = length args) then
-        true
-      else
-        raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
-  | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
+      (case strip_comb u of
+        (Const (_, T), args) =>
+          if (length (binder_types T) = length args) then
+            true
+          else
+            raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
+      | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
   | check_equation_format_term t =
-    raise TERM ("check_equation_format_term failed: Not an equation", [t])
+      raise TERM ("check_equation_format_term failed: Not an equation", [t])
 
 val check_equation_format = check_equation_format_term o prop_of
 
 
 fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
   | defining_term_of_equation_term t =
-    raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
+      raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
 
 val defining_term_of_equation = defining_term_of_equation_term o prop_of
 
 fun defining_const_of_equation th =
-  case defining_term_of_equation th
-   of Const (c, _) => c
-    | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th])
+  (case defining_term_of_equation th of
+    Const (c, _) => c
+  | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th]))
 
 
 
@@ -115,9 +115,10 @@
 (* Normalizing equations *)
 
 fun mk_meta_equation th =
-  case prop_of th of
-    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
-  | _ => th
+  (case prop_of th of
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) =>
+      th RS @{thm eq_reflection}
+  | _ => th)
 
 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
 
@@ -131,13 +132,13 @@
   let
     val res = Name.invent_names ctxt s xs
   in (res, fold Name.declare (map fst res) ctxt) end
-  
+
 fun split_all_pairs thy th =
   let
     val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val ((_, [th']), _) = Variable.import true [th] ctxt
     val t = prop_of th'
-    val frees = Term.add_frees t [] 
+    val frees = Term.add_frees t []
     val freenames = Term.add_free_names t []
     val nctxt = Name.make_context freenames
     fun mk_tuple_rewrites (x, T) nctxt =
@@ -146,7 +147,7 @@
         val (xTs, nctxt') = declare_names x Ts nctxt
         val paths = HOLogic.flat_tupleT_paths T
       in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
-    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
+    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
     val t' = Pattern.rewrite_term thy rewr [] t
     val th'' =
       Goal.prove ctxt (Term.add_free_names t' []) [] t'
@@ -162,7 +163,7 @@
     val ctxt = Proof_Context.init_global thy
     val inline_defs = Predicate_Compile_Inline_Defs.get ctxt
     val th' = (Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs)) th
-    (*val _ = print_step options 
+    (*val _ = print_step options
       ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
        ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
        ^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)
@@ -206,11 +207,13 @@
         else
           NONE
     fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
-    val spec = case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
-      [] => (case Spec_Rules.retrieve ctxt t of
-          [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
-        | ((_, (_, ths)) :: _) => filter_defs ths)
-    | ths => rev ths
+    val spec =
+      (case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
+        [] =>
+          (case Spec_Rules.retrieve ctxt t of
+            [] => error ("No specification for " ^ Syntax.string_of_term_global thy t)
+          | ((_, (_, ths)) :: _) => filter_defs ths)
+      | ths => rev ths)
     val _ =
       if show_intermediate_results options then
         tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
@@ -221,38 +224,38 @@
   end
 
 val logic_operator_names =
-  [@{const_name "=="}, 
+  [@{const_name "=="},
    @{const_name "==>"},
    @{const_name Trueprop},
    @{const_name Not},
    @{const_name HOL.eq},
    @{const_name HOL.implies},
    @{const_name All},
-   @{const_name Ex}, 
+   @{const_name Ex},
    @{const_name HOL.conj},
    @{const_name HOL.disj}]
 
-fun special_cases (c, _) = member (op =) [
-  @{const_name Product_Type.Unity},
-  @{const_name False},
-  @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
-  @{const_name Nat.one_nat_inst.one_nat},
-  @{const_name Orderings.less}, @{const_name Orderings.less_eq},
-  @{const_name Groups.zero},
-  @{const_name Groups.one},  @{const_name Groups.plus},
-  @{const_name Nat.ord_nat_inst.less_eq_nat},
-  @{const_name Nat.ord_nat_inst.less_nat},
-(* FIXME
-  @{const_name number_nat_inst.number_of_nat},
-*)
-  @{const_name Num.Bit0},
-  @{const_name Num.Bit1},
-  @{const_name Num.One},
-  @{const_name Int.zero_int_inst.zero_int},
-  @{const_name List.filter},
-  @{const_name HOL.If},
-  @{const_name Groups.minus}
-  ] c
+fun special_cases (c, _) =
+  member (op =)
+   [@{const_name Product_Type.Unity},
+    @{const_name False},
+    @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
+    @{const_name Nat.one_nat_inst.one_nat},
+    @{const_name Orderings.less}, @{const_name Orderings.less_eq},
+    @{const_name Groups.zero},
+    @{const_name Groups.one},  @{const_name Groups.plus},
+    @{const_name Nat.ord_nat_inst.less_eq_nat},
+    @{const_name Nat.ord_nat_inst.less_nat},
+  (* FIXME
+    @{const_name number_nat_inst.number_of_nat},
+  *)
+    @{const_name Num.Bit0},
+    @{const_name Num.Bit1},
+    @{const_name Num.One},
+    @{const_name Int.zero_int_inst.zero_int},
+    @{const_name List.filter},
+    @{const_name HOL.If},
+    @{const_name Groups.minus}] c
 
 
 fun obtain_specification_graph options thy t =
@@ -306,13 +309,12 @@
       |> map (the o Termtab.lookup mapping)
       |> distinct (eq_list eq_cname);
     val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-    
+
     fun namify consts = map string_of_const consts
       |> commas;
     val prgr = map (fn (consts, constss) =>
-      { name = namify consts, ID = namify consts, dir = "", unfold = true,
-        path = "", parents = map namify constss, content = [] }) conn;
-  in Graph_Display.display_graph prgr end;
+      {name = namify consts, ID = namify consts, dir = "", unfold = true,
+       path = "", parents = map namify constss, content = [] }) conn
+  in Graph_Display.display_graph prgr end
 
-
-end;
+end
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -32,16 +32,16 @@
     SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p)
     handle Pattern.MATCH => NONE) (Item_Net.retrieve net t)
   in
-    case poss_preds of
+    (case poss_preds of
       [p] => SOME p
-    | _ => NONE
+    | _ => NONE)
   end
 
 fun pred_of_function thy name =
-  case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
+  (case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
     [] => NONE
   | [(_, p)] => SOME (fst (dest_Const p))
-  | _ => error ("Multiple matches possible for lookup of constant " ^ name)
+  | _ => error ("Multiple matches possible for lookup of constant " ^ name))
 
 fun defined_const thy name = is_some (pred_of_function thy name)
 
@@ -49,18 +49,18 @@
   Fun_Pred.map (Item_Net.update (f, p))
 
 fun transform_ho_typ (T as Type ("fun", _)) =
-  let
-    val (Ts, T') = strip_type T
-  in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end
-| transform_ho_typ t = t
+      let
+        val (Ts, T') = strip_type T
+      in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end
+  | transform_ho_typ t = t
 
-fun transform_ho_arg arg = 
-  case (fastype_of arg) of
+fun transform_ho_arg arg =
+  (case (fastype_of arg) of
     (T as Type ("fun", _)) =>
       (case arg of
         Free (name, _) => Free (name, transform_ho_typ T)
       | _ => raise Fail "A non-variable term at a higher-order position")
-  | _ => arg
+  | _ => arg)
 
 fun pred_type T =
   let
@@ -88,43 +88,43 @@
     end;
 
 fun keep_functions thy t =
-  case try dest_Const (fst (strip_comb t)) of
+  (case try dest_Const (fst (strip_comb t)) of
     SOME (c, _) => Predicate_Compile_Data.keep_function thy c
-  | _ => false
+  | _ => false)
 
 fun flatten thy lookup_pred t (names, prems) =
   let
     fun lift t (names, prems) =
-      case lookup_pred (Envir.eta_contract t) of
+      (case lookup_pred (Envir.eta_contract t) of
         SOME pred => [(pred, (names, prems))]
       | NONE =>
-        let
-          val (vars, body) = strip_abs t
-          val _ = @{assert} (fastype_of body = body_type (fastype_of body))
-          val absnames = Name.variant_list names (map fst vars)
-          val frees = map2 (curry Free) absnames (map snd vars)
-          val body' = subst_bounds (rev frees, body)
-          val resname = singleton (Name.variant_list (absnames @ names)) "res"
-          val resvar = Free (resname, fastype_of body)
-          val t = flatten' body' ([], [])
-            |> map (fn (res, (inner_names, inner_prems)) =>
-              let
-                fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
-                val vTs = 
-                  fold Term.add_frees inner_prems []
-                  |> filter (fn (x, _) => member (op =) inner_names x)
-                val t = 
-                  fold mk_exists vTs
-                  (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
-                    map HOLogic.dest_Trueprop inner_prems))
-              in
-                t
-              end)
-              |> foldr1 HOLogic.mk_disj
-              |> fold lambda (resvar :: rev frees)
-        in
-          [(t, (names, prems))]
-        end
+          let
+            val (vars, body) = strip_abs t
+            val _ = @{assert} (fastype_of body = body_type (fastype_of body))
+            val absnames = Name.variant_list names (map fst vars)
+            val frees = map2 (curry Free) absnames (map snd vars)
+            val body' = subst_bounds (rev frees, body)
+            val resname = singleton (Name.variant_list (absnames @ names)) "res"
+            val resvar = Free (resname, fastype_of body)
+            val t = flatten' body' ([], [])
+              |> map (fn (res, (inner_names, inner_prems)) =>
+                let
+                  fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
+                  val vTs =
+                    fold Term.add_frees inner_prems []
+                    |> filter (fn (x, _) => member (op =) inner_names x)
+                  val t =
+                    fold mk_exists vTs
+                    (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
+                      map HOLogic.dest_Trueprop inner_prems))
+                in
+                  t
+                end)
+                |> foldr1 HOLogic.mk_disj
+                |> fold lambda (resvar :: rev frees)
+          in
+            [(t, (names, prems))]
+          end)
     and flatten_or_lift (t, T) (names, prems) =
       if fastype_of t = T then
         flatten' t (names, prems)
@@ -134,7 +134,7 @@
           lift t (names, prems)
         else
           error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^
-          ", " ^  Syntax.string_of_typ_global thy T)
+            ", " ^  Syntax.string_of_typ_global thy T)
     and flatten' (t as Const _) (names, prems) = [(t, (names, prems))]
       | flatten' (t as Free _) (names, prems) = [(t, (names, prems))]
       | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))]
@@ -156,7 +156,7 @@
                   (* in general unsound! *)
                   (res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B')) :: prems)))))
             end)
-        | Const (@{const_name "Let"}, _) => 
+        | Const (@{const_name "Let"}, _) =>
             (let
               val (_, [f, g]) = strip_comb t
             in
@@ -199,9 +199,10 @@
             val args = map (Envir.eta_long []) args
             val _ = @{assert} (fastype_of t = body_type (fastype_of t))
             val f' = lookup_pred f
-            val Ts = case f' of
-              SOME pred => (fst (split_last (binder_types (fastype_of pred))))
-            | NONE => binder_types (fastype_of f)
+            val Ts =
+              (case f' of
+                SOME pred => (fst (split_last (binder_types (fastype_of pred))))
+              | NONE => binder_types (fastype_of f))
           in
             folds_map flatten_or_lift (args ~~ Ts) (names, prems) |>
             (case f' of
@@ -272,7 +273,8 @@
       fun mk_intros ((func, pred), (args, rhs)) =
         if (body_type (fastype_of func) = @{typ bool}) then
          (* TODO: preprocess predicate definition of rhs *)
-          [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
+          [Logic.list_implies
+            ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
         else
           let
             val names = Term.add_free_names rhs []
@@ -316,9 +318,10 @@
       let
         (*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*)
         val t = HOLogic.dest_Trueprop prem
-        val (lit, mk_lit) = case try HOLogic.dest_not t of
+        val (lit, mk_lit) =
+          (case try HOLogic.dest_not t of
             SOME t => (t, HOLogic.mk_not)
-          | NONE => (t, I)
+          | NONE => (t, I))
         val (P, args) = strip_comb lit
       in
         folds_map (flatten thy lookup_pred) args (names, [])
@@ -342,4 +345,4 @@
     map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
   end
 
-end;
+end
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -20,15 +20,15 @@
 open Predicate_Compile_Aux
 
 fun is_compound ((Const (@{const_name Not}, _)) $ _) =
-    error "is_compound: Negation should not occur; preprocessing is defect"
+      error "is_compound: Negation should not occur; preprocessing is defect"
   | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
   | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
   | is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
-    error "is_compound: Conjunction should not occur; preprocessing is defect"
+      error "is_compound: Conjunction should not occur; preprocessing is defect"
   | is_compound _ = false
 
 fun try_destruct_case thy names atom =
-  case find_split_thm thy (fst (strip_comb atom)) of
+  (case find_split_thm thy (fst (strip_comb atom)) of
     NONE => NONE
   | SOME raw_split_thm =>
     let
@@ -48,17 +48,17 @@
           val vars = map Free (var_names ~~ (map snd vTs))
           val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
           fun partition_prem_subst prem =
-            case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
+            (case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
               (Free (x, T), r) => (NONE, SOME ((x, T), r))
-            | _ => (SOME prem, NONE)
+            | _ => (SOME prem, NONE))
           fun partition f xs =
             let
               fun partition' acc1 acc2 [] = (rev acc1, rev acc2)
                 | partition' acc1 acc2 (x :: xs) =
                   let
                     val (y, z) = f x
-                    val acc1' = case y of NONE => acc1 | SOME y' => y' :: acc1
-                    val acc2' = case z of NONE => acc2 | SOME z' => z' :: acc2
+                    val acc1' = (case y of NONE => acc1 | SOME y' => y' :: acc1)
+                    val acc2' = (case z of NONE => acc2 | SOME z' => z' :: acc2)
                   in partition' acc1' acc2' xs end
             in partition' [] [] xs end
           val (prems'', subst) = partition partition_prem_subst prems'
@@ -67,18 +67,19 @@
             fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t
           val rhs = Envir.expand_term_frees subst pre_rhs
         in
-          case try_destruct_case thy (var_names @ names') rhs of
+          (case try_destruct_case thy (var_names @ names') rhs of
             NONE => [(subst, rhs)]
-          | SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs
+          | SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs)
         end
-     in SOME (atom', maps mk_subst_rhs assms) end
+     in SOME (atom', maps mk_subst_rhs assms) end)
      
 fun flatten constname atom (defs, thy) =
   if is_compound atom then
     let
       val atom = Envir.beta_norm (Envir.eta_long [] atom)
-      val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
-        ((Long_Name.base_name constname) ^ "_aux")
+      val constname =
+        singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
+          ((Long_Name.base_name constname) ^ "_aux")
       val full_constname = Sign.full_bname thy constname
       val (params, args) = List.partition (is_predT o fastype_of)
         (map Free (Term.add_frees atom []))
@@ -92,7 +93,7 @@
       (lhs, ((full_constname, [definition]) :: defs, thy'))
     end
   else
-    case (fst (strip_comb atom)) of
+    (case (fst (strip_comb atom)) of
       (Const (@{const_name If}, _)) =>
         let
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
@@ -103,28 +104,28 @@
           flatten constname atom' (defs, thy)
         end
     | _ =>
-      case try_destruct_case thy [] atom of
-        NONE => (atom, (defs, thy))
-      | SOME (atom', srs) =>
-        let      
-          val frees = map Free (Term.add_frees atom' [])
-          val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
-           ((Long_Name.base_name constname) ^ "_aux")
-          val full_constname = Sign.full_bname thy constname
-          val constT = map fastype_of frees ---> HOLogic.boolT
-          val lhs = list_comb (Const (full_constname, constT), frees)
-          fun mk_def (subst, rhs) =
-            Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
-          val new_defs = map mk_def srs
-          val (definition, thy') = thy
-          |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-          |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
-            (map_index (fn (i, t) =>
-              ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
-        in
-          (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
-        end
-
+        (case try_destruct_case thy [] atom of
+          NONE => (atom, (defs, thy))
+        | SOME (atom', srs) =>
+            let      
+              val frees = map Free (Term.add_frees atom' [])
+              val constname =
+                singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
+                  ((Long_Name.base_name constname) ^ "_aux")
+              val full_constname = Sign.full_bname thy constname
+              val constT = map fastype_of frees ---> HOLogic.boolT
+              val lhs = list_comb (Const (full_constname, constT), frees)
+              fun mk_def (subst, rhs) =
+                Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
+              val new_defs = map mk_def srs
+              val (definition, thy') = thy
+              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+              |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
+                (map_index (fn (i, t) =>
+                  ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
+            in
+              (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
+            end))
 
 fun flatten_intros constname intros thy =
   let
@@ -143,7 +144,7 @@
 (* TODO: same function occurs in inductive package *)
 fun select_disj 1 1 = []
   | select_disj _ 1 = [rtac @{thm disjI1}]
-  | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1));
+  | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1))
 
 fun introrulify thy ths = 
   let
@@ -258,8 +259,9 @@
                 |> process constname t1 
                 ||>> process constname t2
                 |>> HOLogic.mk_prod
-            | NONE => (warning ("Replacing higher order arguments " ^
-              "is not applied in an undestructable product type"); (arg, (new_defs, thy))))
+            | NONE =>
+              (warning ("Replacing higher order arguments " ^
+                "is not applied in an undestructable product type"); (arg, (new_defs, thy))))
           else if (is_predT (fastype_of arg)) then
             process constname arg (new_defs, thy)
           else
@@ -274,7 +276,8 @@
       let
         val constname = fst (dest_Const (fst (strip_comb
           (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro))))))
-        val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
+        val (intro_ts, (new_defs, thy)) =
+          fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
         val th = Skip_Proof.make_thm thy intro_ts
       in
         (th, (new_defs, thy))
@@ -290,4 +293,4 @@
     (intross', (new_defs, thy'))
   end
 
-end;
+end
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -22,28 +22,34 @@
 open Core_Data;
 open Mode_Inference;
 
+
 (* debug stuff *)
 
 fun print_tac options s = 
   if show_proof_trace options then Tactical.print_tac s else Seq.single;
 
+
 (** auxiliary **)
 
 datatype assertion = Max_number_of_subgoals of int
+
 fun assert_tac (Max_number_of_subgoals i) st =
   if (nprems_of st <= i) then Seq.single st
-  else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
-    ^ "\n" ^ Pretty.string_of (Pretty.chunks
-      (Goal_Display.pretty_goals_without_context st)));
+  else
+    raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :\n" ^
+      Pretty.string_of (Pretty.chunks
+        (Goal_Display.pretty_goals_without_context st)))
 
 
 (** special setup for simpset **)
+
 val HOL_basic_ss' =
   simpset_of (put_simpset HOL_basic_ss @{context}
     addsimps @{thms simp_thms Pair_eq}
     setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
     setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI})))
 
+
 (* auxillary functions *)
 
 fun is_Type (Type _) = true
@@ -53,15 +59,18 @@
 (* which then consequently would be splitted *)
 (* else false *)
 fun is_constructor thy t =
-  if (is_Type (fastype_of t)) then
+  if is_Type (fastype_of t) then
     (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
       NONE => false
-    | SOME info => (let
-      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
-      val (c, _) = strip_comb t
-      in (case c of
-        Const (name, _) => member (op =) constr_consts name
-        | _ => false) end))
+    | SOME info =>
+        let
+          val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
+          val (c, _) = strip_comb t
+        in
+          (case c of
+            Const (name, _) => member (op =) constr_consts name
+          | _ => false)
+        end)
   else false
 
 (* MAJOR FIXME:  prove_params should be simple
@@ -73,19 +82,20 @@
     val mode = head_mode_of deriv
     val param_derivations = param_derivations_of deriv
     val ho_args = ho_args_of mode args
-    val f_tac = case f of
-      Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
-         [@{thm eval_pred}, predfun_definition_of ctxt name mode,
-         @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
-         @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
-    | Free _ =>
-      Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
-        let
-          val prems' = maps dest_conjunct_prem (take nargs prems)
-        in
-          rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
-        end) ctxt 1
-    | Abs _ => raise Fail "prove_param: No valid parameter term"
+    val f_tac =
+      (case f of
+        Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
+           [@{thm eval_pred}, predfun_definition_of ctxt name mode,
+           @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
+           @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
+      | Free _ =>
+        Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
+          let
+            val prems' = maps dest_conjunct_prem (take nargs prems)
+          in
+            rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+          end) ctxt 1
+      | Abs _ => raise Fail "prove_param: No valid parameter term")
   in
     REPEAT_DETERM (rtac @{thm ext} 1)
     THEN print_tac options "prove_param"
@@ -97,7 +107,7 @@
   end
 
 fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
-  case strip_comb t of
+  (case strip_comb t of
     (Const (name, _), args) =>
       let
         val mode = head_mode_of deriv
@@ -117,25 +127,25 @@
         THEN (REPEAT_DETERM (atac 1))
       end
   | (Free _, _) =>
-    print_tac options "proving parameter call.."
-    THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
-        let
-          val param_prem = nth prems premposition
-          val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
-          val prems' = maps dest_conjunct_prem (take nargs prems)
-          fun param_rewrite prem =
-            param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
-          val SOME rew_eq = find_first param_rewrite prems'
-          val param_prem' = rewrite_rule ctxt'
-            (map (fn th => th RS @{thm eq_reflection})
-              [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
-            param_prem
-        in
-          rtac param_prem' 1
-        end) ctxt 1
-    THEN print_tac options "after prove parameter call"
+      print_tac options "proving parameter call.."
+      THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
+          let
+            val param_prem = nth prems premposition
+            val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
+            val prems' = maps dest_conjunct_prem (take nargs prems)
+            fun param_rewrite prem =
+              param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
+            val SOME rew_eq = find_first param_rewrite prems'
+            val param_prem' = rewrite_rule ctxt'
+              (map (fn th => th RS @{thm eq_reflection})
+                [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
+              param_prem
+          in
+            rtac param_prem' 1
+          end) ctxt 1
+      THEN print_tac options "after prove parameter call")
 
-fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
+fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st
 
 fun prove_match options ctxt nargs out_ts =
   let
@@ -154,7 +164,7 @@
       (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
   (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   in
-     (* make this simpset better! *)
+    (* make this simpset better! *)
     asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
     THEN print_tac options "after prove_match:"
     THEN (DETERM (TRY 
@@ -176,15 +186,17 @@
     THEN print_tac options "after if simplification"
   end;
 
+
 (* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
 
 fun prove_sidecond ctxt t =
   let
-    fun preds_of t nameTs = case strip_comb t of 
-      (Const (name, T), args) =>
-        if is_registered ctxt name then (name, T) :: nameTs
-          else fold preds_of args nameTs
-      | _ => nameTs
+    fun preds_of t nameTs =
+      (case strip_comb t of
+        (Const (name, T), args) =>
+          if is_registered ctxt name then (name, T) :: nameTs
+            else fold preds_of args nameTs
+      | _ => nameTs)
     val preds = preds_of t []
     val defs = map
       (fn (pred, T) => predfun_definition_of ctxt pred
@@ -200,88 +212,88 @@
   let
     val (in_ts, clause_out_ts) = split_mode mode ts;
     fun prove_prems out_ts [] =
-      (prove_match options ctxt nargs out_ts)
-      THEN print_tac options "before simplifying assumptions"
-      THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
-      THEN print_tac options "before single intro rule"
-      THEN Subgoal.FOCUS_PREMS
-         (fn {context = ctxt', params, prems, asms, concl, schematics} =>
-          let
-            val prems' = maps dest_conjunct_prem (take nargs prems)
-          in
-            rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
-          end) ctxt 1
-      THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
-    | prove_prems out_ts ((p, deriv) :: ps) =
-      let
-        val premposition = (find_index (equal p) clauses) + nargs
-        val mode = head_mode_of deriv
-        val rest_tac =
-          rtac @{thm bindI} 1
-          THEN (case p of Prem t =>
-            let
-              val (_, us) = strip_comb t
-              val (_, out_ts''') = split_mode mode us
-              val rec_tac = prove_prems out_ts''' ps
-            in
-              print_tac options "before clause:"
-              (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
-              THEN print_tac options "before prove_expr:"
-              THEN prove_expr options ctxt nargs premposition (t, deriv)
-              THEN print_tac options "after prove_expr:"
-              THEN rec_tac
-            end
-          | Negprem t =>
+        (prove_match options ctxt nargs out_ts)
+        THEN print_tac options "before simplifying assumptions"
+        THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
+        THEN print_tac options "before single intro rule"
+        THEN Subgoal.FOCUS_PREMS
+           (fn {context = ctxt', params, prems, asms, concl, schematics} =>
             let
-              val (t, args) = strip_comb t
-              val (_, out_ts''') = split_mode mode args
-              val rec_tac = prove_prems out_ts''' ps
-              val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
-              val neg_intro_rule =
-                Option.map (fn name =>
-                  the (predfun_neg_intro_of ctxt name mode)) name
-              val param_derivations = param_derivations_of deriv
-              val params = ho_args_of mode args
+              val prems' = maps dest_conjunct_prem (take nargs prems)
             in
-              print_tac options "before prove_neg_expr:"
-              THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
-                [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
-                 @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
-              THEN (if (is_some name) then
-                  print_tac options "before applying not introduction rule"
-                  THEN Subgoal.FOCUS_PREMS
-                    (fn {context, params = params, prems, asms, concl, schematics} =>
-                      rtac (the neg_intro_rule) 1
-                      THEN rtac (nth prems premposition) 1) ctxt 1
-                  THEN print_tac options "after applying not introduction rule"
-                  THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
-                  THEN (REPEAT_DETERM (atac 1))
-                else
-                  rtac @{thm not_predI'} 1
-                  (* test: *)
-                  THEN dtac @{thm sym} 1
-                  THEN asm_full_simp_tac
-                    (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1)
-                  THEN simp_tac
-                    (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
-              THEN rec_tac
-            end
-          | Sidecond t =>
-           rtac @{thm if_predI} 1
-           THEN print_tac options "before sidecond:"
-           THEN prove_sidecond ctxt t
-           THEN print_tac options "after sidecond:"
-           THEN prove_prems [] ps)
-      in (prove_match options ctxt nargs out_ts)
-          THEN rest_tac
-      end;
+              rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+            end) ctxt 1
+        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
+    | prove_prems out_ts ((p, deriv) :: ps) =
+        let
+          val premposition = (find_index (equal p) clauses) + nargs
+          val mode = head_mode_of deriv
+          val rest_tac =
+            rtac @{thm bindI} 1
+            THEN (case p of Prem t =>
+              let
+                val (_, us) = strip_comb t
+                val (_, out_ts''') = split_mode mode us
+                val rec_tac = prove_prems out_ts''' ps
+              in
+                print_tac options "before clause:"
+                (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
+                THEN print_tac options "before prove_expr:"
+                THEN prove_expr options ctxt nargs premposition (t, deriv)
+                THEN print_tac options "after prove_expr:"
+                THEN rec_tac
+              end
+            | Negprem t =>
+              let
+                val (t, args) = strip_comb t
+                val (_, out_ts''') = split_mode mode args
+                val rec_tac = prove_prems out_ts''' ps
+                val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
+                val neg_intro_rule =
+                  Option.map (fn name =>
+                    the (predfun_neg_intro_of ctxt name mode)) name
+                val param_derivations = param_derivations_of deriv
+                val params = ho_args_of mode args
+              in
+                print_tac options "before prove_neg_expr:"
+                THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
+                  [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
+                   @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
+                THEN (if (is_some name) then
+                    print_tac options "before applying not introduction rule"
+                    THEN Subgoal.FOCUS_PREMS
+                      (fn {context, params = params, prems, asms, concl, schematics} =>
+                        rtac (the neg_intro_rule) 1
+                        THEN rtac (nth prems premposition) 1) ctxt 1
+                    THEN print_tac options "after applying not introduction rule"
+                    THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
+                    THEN (REPEAT_DETERM (atac 1))
+                  else
+                    rtac @{thm not_predI'} 1
+                    (* test: *)
+                    THEN dtac @{thm sym} 1
+                    THEN asm_full_simp_tac
+                      (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1)
+                    THEN simp_tac
+                      (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
+                THEN rec_tac
+              end
+            | Sidecond t =>
+             rtac @{thm if_predI} 1
+             THEN print_tac options "before sidecond:"
+             THEN prove_sidecond ctxt t
+             THEN print_tac options "after sidecond:"
+             THEN prove_prems [] ps)
+        in (prove_match options ctxt nargs out_ts)
+            THEN rest_tac
+        end
     val prems_tac = prove_prems in_ts moded_ps
   in
     print_tac options "Proving clause..."
     THEN rtac @{thm bindI} 1
     THEN rtac @{thm singleI} 1
     THEN prems_tac
-  end;
+  end
 
 fun select_sup 1 1 = []
   | select_sup _ 1 = [rtac @{thm supI1}]
@@ -303,7 +315,8 @@
              (1 upto (length moded_clauses))))
     THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
     THEN print_tac options "proved one direction"
-  end;
+  end
+
 
 (** Proof in the other direction **)
 
@@ -348,12 +361,13 @@
     val mode = head_mode_of deriv
     val param_derivations = param_derivations_of deriv
     val ho_args = ho_args_of mode args
-    val f_tac = case f of
+    val f_tac =
+      (case f of
         Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps 
            (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
            :: @{thm "Product_Type.split_conv"}::[])) 1
       | Free _ => all_tac
-      | _ => error "prove_param2: illegal parameter term"
+      | _ => error "prove_param2: illegal parameter term")
   in
     print_tac options "before simplification in prove_args:"
     THEN f_tac
@@ -379,23 +393,25 @@
         end
       | _ => etac @{thm bindE} 1)
 
-fun prove_sidecond2 options ctxt t = let
-  fun preds_of t nameTs = case strip_comb t of 
-    (Const (name, T), args) =>
-      if is_registered ctxt name then (name, T) :: nameTs
-        else fold preds_of args nameTs
-    | _ => nameTs
-  val preds = preds_of t []
-  val defs = map
-    (fn (pred, T) => predfun_definition_of ctxt pred 
-      (all_input_of T))
-      preds
+fun prove_sidecond2 options ctxt t =
+  let
+    fun preds_of t nameTs =
+      (case strip_comb t of
+        (Const (name, T), args) =>
+          if is_registered ctxt name then (name, T) :: nameTs
+            else fold preds_of args nameTs
+      | _ => nameTs)
+    val preds = preds_of t []
+    val defs = map
+      (fn (pred, T) => predfun_definition_of ctxt pred 
+        (all_input_of T))
+        preds
   in
-   (* only simplify the one assumption *)
-   full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1 
-   (* need better control here! *)
-   THEN print_tac options "after sidecond2 simplification"
-   end
+    (* only simplify the one assumption *)
+    full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1 
+    (* need better control here! *)
+    THEN print_tac options "after sidecond2 simplification"
+  end
   
 fun prove_clause2 options ctxt pred mode (ts, ps) i =
   let
@@ -426,46 +442,48 @@
     | prove_prems2 out_ts ((p, deriv) :: ps) =
       let
         val mode = head_mode_of deriv
-        val rest_tac = (case p of
-          Prem t =>
-          let
-            val (_, us) = strip_comb t
-            val (_, out_ts''') = split_mode mode us
-            val rec_tac = prove_prems2 out_ts''' ps
-          in
-            (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
-          end
-        | Negprem t =>
-          let
-            val (_, args) = strip_comb t
-            val (_, out_ts''') = split_mode mode args
-            val rec_tac = prove_prems2 out_ts''' ps
-            val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
-            val param_derivations = param_derivations_of deriv
-            val ho_args = ho_args_of mode args
-          in
-            print_tac options "before neg prem 2"
-            THEN etac @{thm bindE} 1
-            THEN (if is_some name then
-                full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
-                  [predfun_definition_of ctxt (the name) mode]) 1
-                THEN etac @{thm not_predE} 1
-                THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
-                THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
-              else
-                etac @{thm not_predE'} 1)
-            THEN rec_tac
-          end 
-        | Sidecond t =>
-          etac @{thm bindE} 1
-          THEN etac @{thm if_predE} 1
-          THEN prove_sidecond2 options ctxt t
-          THEN prove_prems2 [] ps)
-      in print_tac options "before prove_match2:"
-         THEN prove_match2 options ctxt out_ts
-         THEN print_tac options "after prove_match2:"
-         THEN rest_tac
-      end;
+        val rest_tac =
+          (case p of
+            Prem t =>
+              let
+                val (_, us) = strip_comb t
+                val (_, out_ts''') = split_mode mode us
+                val rec_tac = prove_prems2 out_ts''' ps
+              in
+                (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
+              end
+          | Negprem t =>
+              let
+                val (_, args) = strip_comb t
+                val (_, out_ts''') = split_mode mode args
+                val rec_tac = prove_prems2 out_ts''' ps
+                val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
+                val param_derivations = param_derivations_of deriv
+                val ho_args = ho_args_of mode args
+              in
+                print_tac options "before neg prem 2"
+                THEN etac @{thm bindE} 1
+                THEN (if is_some name then
+                    full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
+                      [predfun_definition_of ctxt (the name) mode]) 1
+                    THEN etac @{thm not_predE} 1
+                    THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
+                    THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
+                  else
+                    etac @{thm not_predE'} 1)
+                THEN rec_tac
+              end 
+          | Sidecond t =>
+              etac @{thm bindE} 1
+              THEN etac @{thm if_predE} 1
+              THEN prove_sidecond2 options ctxt t
+              THEN prove_prems2 [] ps)
+      in
+        print_tac options "before prove_match2:"
+        THEN prove_match2 options ctxt out_ts
+        THEN print_tac options "after prove_match2:"
+        THEN rest_tac
+      end
     val prems_tac = prove_prems2 in_ts ps 
   in
     print_tac options "starting prove_clause2"
@@ -489,14 +507,15 @@
      THEN (
        if null moded_clauses then etac @{thm botE} 1
        else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
-  end;
+  end
+
 
 (** proof procedure **)
 
 fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
   let
     val ctxt = Proof_Context.init_global thy   (* FIXME proper context!? *)
-    val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
+    val clauses = (case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [])
   in
     Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
       (if not (skip_proof options) then
@@ -508,6 +527,6 @@
         THEN prove_other_direction options ctxt pred mode moded_clauses
         THEN print_tac options "proved other direction")
       else (fn _ => ALLGOALS Skip_Proof.cheat_tac))
-  end;
+  end
 
-end;
\ No newline at end of file
+end
\ No newline at end of file
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -9,24 +9,28 @@
   type seed = Random_Engine.seed
   (*val quickcheck : Proof.context -> term -> int -> term list option*)
   val put_pred_result :
-    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred) ->
-      Proof.context -> Proof.context;
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+      term list Predicate.pred) ->
+    Proof.context -> Proof.context
   val put_dseq_result :
-    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed) ->
-      Proof.context -> Proof.context;
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+      term list Limited_Sequence.dseq * seed) ->
+    Proof.context -> Proof.context
   val put_lseq_result :
-    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
-      Proof.context -> Proof.context;
-  val put_new_dseq_result : (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
+      term list Lazy_Sequence.lazy_sequence) ->
+    Proof.context -> Proof.context
+  val put_new_dseq_result :
+    (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
   val put_cps_result : (unit -> Code_Numeral.natural -> (bool * term list) option) ->
     Proof.context -> Proof.context
   val test_goals : (Predicate_Compile_Aux.compilation * bool) ->
-    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
-      -> Quickcheck.result list
-  val nrandom : int Unsynchronized.ref;
-  val debug : bool Unsynchronized.ref;
-  val no_higher_order_predicate : string list Unsynchronized.ref;
+    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list ->
+    Quickcheck.result list
+  val nrandom : int Unsynchronized.ref
+  val debug : bool Unsynchronized.ref
+  val no_higher_order_predicate : string list Unsynchronized.ref
   val setup : theory -> theory
 end;
 
@@ -44,48 +48,48 @@
   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Pred_Result"
-);
-val put_pred_result = Pred_Result.put;
+)
+val put_pred_result = Pred_Result.put
 
 structure Dseq_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Dseq_Result"
-);
-val put_dseq_result = Dseq_Result.put;
+)
+val put_dseq_result = Dseq_Result.put
 
 structure Lseq_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Lseq_Result"
-);
-val put_lseq_result = Lseq_Result.put;
+)
+val put_lseq_result = Lseq_Result.put
 
 structure New_Dseq_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "New_Dseq_Random_Result"
-);
-val put_new_dseq_result = New_Dseq_Result.put;
+)
+val put_new_dseq_result = New_Dseq_Result.put
 
 structure CPS_Result = Proof_Data
 (
   type T = unit -> Code_Numeral.natural -> (bool * term list) option
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "CPS_Result"
-);
-val put_cps_result = CPS_Result.put;
+)
+val put_cps_result = CPS_Result.put
 
 val target = "Quickcheck"
 
-val nrandom = Unsynchronized.ref 3;
+val nrandom = Unsynchronized.ref 3
 
-val debug = Unsynchronized.ref false;
+val debug = Unsynchronized.ref false
 
-val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
+val no_higher_order_predicate = Unsynchronized.ref ([] : string list)
 
 val options = Options {
   expected_modes = NONE,
@@ -98,7 +102,7 @@
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
-  show_invalid_clauses = false, 
+  show_invalid_clauses = false,
   skip_proof = false,
   compilation = Random,
   inductify = true,
@@ -141,7 +145,7 @@
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
     show_invalid_clauses = s_ic, skip_proof = s_p,
-    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = _, 
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = _,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
@@ -157,7 +161,7 @@
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
     show_invalid_clauses = s_ic, skip_proof = s_p,
-    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = _, no_higher_order_predicate = no_ho,
     smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
@@ -173,7 +177,7 @@
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
     show_invalid_clauses = s_ic, skip_proof = s_p,
-    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
+    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = _,
     smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
@@ -185,7 +189,7 @@
     smart_depth_limiting = sm_dl, no_topmost_reordering = re})
 
 
-fun get_options () = 
+fun get_options () =
   set_no_higher_order_predicate (!no_higher_order_predicate)
     (if !debug then debug_options else options)
 
@@ -210,7 +214,7 @@
   Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
 val mk_gen_bind =
   Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
-  
+
 
 val mk_cpsT =
   Predicate_Compile_Aux.mk_monadT Pos_Bounded_CPS_Comp_Funs.compfuns
@@ -251,41 +255,41 @@
       if member eq_mode modes output_mode then
         let
           val name = Core_Data.function_name_of compilation ctxt4 full_constname output_mode
-          val T = 
-            case compilation of
+          val T =
+            (case compilation of
               Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))
             | New_Pos_Random_DSeq => mk_new_randompredT (HOLogic.mk_tupleT (map snd vs'))
             | Pos_Generator_DSeq => mk_new_dseqT (HOLogic.mk_tupleT (map snd vs'))
             | Depth_Limited_Random =>
-              [@{typ natural}, @{typ natural}, @{typ natural},
-              @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
-            | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs'))
+                [@{typ natural}, @{typ natural}, @{typ natural},
+                 @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
+            | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs')))
         in
           Const (name, T)
         end
       else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
     fun mk_Some T = Const (@{const_name "Option.Some"}, T --> Type (@{type_name "Option.option"}, [T]))
     val qc_term =
-      case compilation of
-          Pos_Random_DSeq => mk_bind (prog,
-            mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
-            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
-        | New_Pos_Random_DSeq => mk_new_bind (prog,
-            mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
-            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
-        | Pos_Generator_DSeq => mk_gen_bind (prog,
-            mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
-            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
-        | Pos_Generator_CPS => prog $
-            mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $
-            HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term}
-                (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))     
-        | Depth_Limited_Random => fold_rev absdummy
-            [@{typ natural}, @{typ natural}, @{typ natural},
-             @{typ Random.seed}]
-            (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
-            mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
-            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
+      (case compilation of
+        Pos_Random_DSeq => mk_bind (prog,
+          mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
+          (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+      | New_Pos_Random_DSeq => mk_new_bind (prog,
+          mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
+          (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+      | Pos_Generator_DSeq => mk_gen_bind (prog,
+          mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
+          (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+      | Pos_Generator_CPS => prog $
+          mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $
+          HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term}
+              (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))
+      | Depth_Limited_Random => fold_rev absdummy
+          [@{typ natural}, @{typ natural}, @{typ natural},
+           @{typ Random.seed}]
+          (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
+          mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
+          (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))))
     val prog =
       case compilation of
         Pos_Random_DSeq =>
@@ -310,7 +314,7 @@
                   g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
                   qc_term []
           in
-            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
+            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield
                (
                let
                  val seed = Random_Engine.next_seed ()
@@ -346,7 +350,7 @@
                   g depth nrandom size seed |> (Predicate.map o map) proc)
                 qc_term []
           in
-            fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield 
+            fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield
               (compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
           end
   in
@@ -368,14 +372,14 @@
          val _ = if Config.get ctxt Quickcheck.timing then
            message (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
         in
-          case result of NONE => try' (i + 1) | SOME q => SOME q
+          (case result of NONE => try' (i + 1) | SOME q => SOME q)
         end
-      else
-        NONE
+      else NONE
   in
     try' 0
   end
 
+
 (* quickcheck interface functions *)
 
 fun compile_term' compilation options ctxt (t, _) =
@@ -386,7 +390,8 @@
       (Code_Numeral.natural_of_integer (!nrandom)) o Code_Numeral.natural_of_integer)
   in
     Quickcheck.Result
-      {counterexample = Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample,
+      {counterexample =
+        Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample,
        evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
   end
 
@@ -412,14 +417,16 @@
       (maps (map snd) correct_inst_goals) []
   end
 
-val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true);
-val smart_slow_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false);
+val smart_exhaustive_active =
+  Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true)
+val smart_slow_exhaustive_active =
+  Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false)
 
 val setup =
-  Exhaustive_Generators.setup_exhaustive_datatype_interpretation 
+  Exhaustive_Generators.setup_exhaustive_datatype_interpretation
   #> Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
     (smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
   #> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
     (smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false))))
 
-end;
+end
diff -r 9781e17dcc23 -r 3fd63b92ea3b src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Feb 12 13:33:05 2014 +0100
@@ -6,7 +6,8 @@
 
 signature PREDICATE_COMPILE_SPECIALISATION =
 sig
-  val find_specialisations : string list -> (string * thm list) list -> theory -> (string * thm list) list * theory
+  val find_specialisations : string list -> (string * thm list) list ->
+    theory -> (string * thm list) list * theory
 end;
 
 structure Predicate_Compile_Specialisation : PREDICATE_COMPILE_SPECIALISATION =
@@ -17,10 +18,10 @@
 (* table of specialisations *)
 structure Specialisations = Theory_Data
 (
-  type T = (term * term) Item_Net.T;
-  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
-  val extend = I;
-  val merge = Item_Net.merge;
+  type T = (term * term) Item_Net.T
+  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst)
+  val extend = I
+  val merge = Item_Net.merge
 )
 
 fun specialisation_of thy atom =
@@ -29,7 +30,8 @@
 fun import (_, intros) args ctxt =
   let
     val ((_, intros'), ctxt') = Variable.importT intros ctxt
-    val pred' = fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
+    val pred' =
+      fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
     val Ts = binder_types (fastype_of pred')
     val argTs = map fastype_of args
     val Tsubst = Type.raw_matches (argTs, Ts) Vartab.empty
@@ -44,17 +46,19 @@
     val cnstrs = flat (maps
       (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
       (Symtab.dest (Datatype.get_all thy)));
-    fun check t = (case strip_comb t of
+    fun check t =
+      (case strip_comb t of
         (Var _, []) => (true, true)
       | (Free _, []) => (true, true)
       | (Const (@{const_name Pair}, _), ts) =>
         pairself (forall I) (split_list (map check ts))
-      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
+      | (Const (s, T), ts) =>
+          (case (AList.lookup (op =) cnstrs s, body_type T) of
             (SOME (i, Tname), Type (Tname', _)) => (false,
               length ts = i andalso Tname = Tname' andalso forall (snd o check) ts)
           | _ => (false, false))
       | _ => (false, false))
-  in check t = (false, true) end;
+  in check t = (false, true) end
 
 fun specialise_intros black_list (pred, intros) pats thy =
   let
@@ -91,7 +95,8 @@
         SOME intro
       end handle Pattern.Unif => NONE)
     val specialised_intros_t = map_filter I (map specialise_intro intros)
-    val thy' = Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
+    val thy' =
+      Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
     val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t
     val exported_intros = Variable.exportT ctxt' ctxt specialised_intros
     val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
@@ -124,29 +129,31 @@
       end
     and restrict_pattern' thy [] free_names = ([], free_names)
       | restrict_pattern' thy ((T, Free (x, _)) :: Tts) free_names =
-      let
-        val (ts', free_names') = restrict_pattern' thy Tts free_names
-      in
-        (Free (x, T) :: ts', free_names')
-      end
+          let
+            val (ts', free_names') = restrict_pattern' thy Tts free_names
+          in
+            (Free (x, T) :: ts', free_names')
+          end
       | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
-        replace_term_and_restrict thy T t Tts free_names
+          replace_term_and_restrict thy T t Tts free_names
       | restrict_pattern' thy ((T as Type (Tcon, _), t) :: Tts) free_names =
-        case Datatype.get_constrs thy Tcon of
-          NONE => replace_term_and_restrict thy T t Tts free_names
-        | SOME constrs => (case strip_comb t of
-          (Const (s, _), ats) => (case AList.lookup (op =) constrs s of
-            SOME constr_T =>
-              let
-                val (Ts', T') = strip_type constr_T
-                val Tsubst = Type.raw_match (T', T) Vartab.empty
-                val Ts = map (Envir.subst_type Tsubst) Ts'
-                val (bts', free_names') = restrict_pattern' thy ((Ts ~~ ats) @ Tts) free_names
-                val (ats', ts') = chop (length ats) bts'
-              in
-                (list_comb (Const (s, map fastype_of ats' ---> T), ats') :: ts', free_names')
-              end
-            | NONE => replace_term_and_restrict thy T t Tts free_names))
+          (case Datatype.get_constrs thy Tcon of
+            NONE => replace_term_and_restrict thy T t Tts free_names
+          | SOME constrs =>
+              (case strip_comb t of
+                (Const (s, _), ats) =>
+                  (case AList.lookup (op =) constrs s of
+                    SOME constr_T =>
+                      let
+                        val (Ts', T') = strip_type constr_T
+                        val Tsubst = Type.raw_match (T', T) Vartab.empty
+                        val Ts = map (Envir.subst_type Tsubst) Ts'
+                        val (bts', free_names') = restrict_pattern' thy ((Ts ~~ ats) @ Tts) free_names
+                        val (ats', ts') = chop (length ats) bts'
+                      in
+                        (list_comb (Const (s, map fastype_of ats' ---> T), ats') :: ts', free_names')
+                      end
+                    | NONE => replace_term_and_restrict thy T t Tts free_names)))
     fun restrict_pattern thy Ts args =
       let
         val args = map Logic.unvarify_global args
@@ -155,42 +162,42 @@
         val (pat, _) = restrict_pattern' thy (Ts ~~ args) free_names
       in map Logic.varify_global pat end
     fun detect' atom thy =
-      case strip_comb atom of
+      (case strip_comb atom of
         (pred as Const (pred_name, _), args) =>
           let
-          val Ts = binder_types (Sign.the_const_type thy pred_name)
-          val pats = restrict_pattern thy Ts args
-        in
-          if (exists (is_nontrivial_constrt thy) pats)
-            orelse (has_duplicates (op =) (fold add_vars pats [])) then
-            let
-              val thy' =
-                case specialisation_of thy atom of
-                  [] =>
-                    if member (op =) ((map fst specs) @ black_list) pred_name then
-                      thy
-                    else
-                      (case try (Core_Data.intros_of (Proof_Context.init_global thy)) pred_name of
-                        NONE => thy
-                      | SOME [] => thy
-                      | SOME intros =>
-                          specialise_intros ((map fst specs) @ (pred_name :: black_list))
-                            (pred, intros) pats thy)
-                  | _ :: _ => thy
+            val Ts = binder_types (Sign.the_const_type thy pred_name)
+            val pats = restrict_pattern thy Ts args
+          in
+            if (exists (is_nontrivial_constrt thy) pats)
+              orelse (has_duplicates (op =) (fold add_vars pats [])) then
+              let
+                val thy' =
+                  (case specialisation_of thy atom of
+                    [] =>
+                      if member (op =) ((map fst specs) @ black_list) pred_name then
+                        thy
+                      else
+                        (case try (Core_Data.intros_of (Proof_Context.init_global thy)) pred_name of
+                          NONE => thy
+                        | SOME [] => thy
+                        | SOME intros =>
+                            specialise_intros ((map fst specs) @ (pred_name :: black_list))
+                              (pred, intros) pats thy)
+                  | _ :: _ => thy)
                 val atom' =
-                  case specialisation_of thy' atom of
+                  (case specialisation_of thy' atom of
                     [] => atom
                   | (t, specialised_t) :: _ =>
                     let
                       val subst = Pattern.match thy' (t, atom) (Vartab.empty, Vartab.empty)
-                    in Envir.subst_term subst specialised_t end handle Pattern.MATCH => atom
-                    (*FIXME: this exception could be caught earlier in specialisation_of *)
-            in
-              (atom', thy')
-            end
-          else (atom, thy)
-        end
-      | _ => (atom, thy)
+                    in Envir.subst_term subst specialised_t end handle Pattern.MATCH => atom)
+                    (*FIXME: this exception could be handled earlier in specialisation_of *)
+              in
+                (atom', thy')
+              end
+            else (atom, thy)
+          end
+      | _ => (atom, thy))
     fun specialise' (constname, intros) thy =
       let
         (* FIXME: only necessary because of sloppy Logic.unvarify in restrict_pattern *)