# HG changeset patch
# User wenzelm
# Date 1392921140 -3600
# Node ID 95c8ef02f04b4827229653c6a7ce0f328abd40d4
# Parent  0e2b7f04c9440caca399607b38a6923a9ffd5964
tuned whitespace;

diff -r 0e2b7f04c944 -r 95c8ef02f04b src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Thu Feb 20 18:23:32 2014 +0100
+++ b/src/Tools/coherent.ML	Thu Feb 20 19:32:20 2014 +0100
@@ -91,80 +91,82 @@
   let
     val vs = fold Term.add_vars (maps snd cs) [];
     fun insts [] inst = Seq.single inst
-      | insts ((ixn, T) :: vs') inst = Seq.maps
-          (fn t => insts vs' (((ixn, T), t) :: inst))
-          (Seq.of_list (case Typtab.lookup dom T of
-             NONE => error ("Unknown domain: " ^
-               Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
-               commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
-           | SOME ts => ts))
-  in Seq.map (fn inst =>
-    (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
-      (insts vs [])
+      | insts ((ixn, T) :: vs') inst =
+          Seq.maps (fn t => insts vs' (((ixn, T), t) :: inst))
+            (Seq.of_list
+              (case Typtab.lookup dom T of
+                NONE =>
+                  error ("Unknown domain: " ^
+                    Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
+                    commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
+              | SOME ts => ts))
+  in
+    Seq.map (fn inst =>
+      (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
+        (insts vs [])
   end;
 
 (* Check whether disjunction is valid in given state *)
 fun is_valid_disj ctxt facts [] = false
   | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
-      let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts
-      in case Seq.pull (valid_conj ctxt facts empty_env
-        (map (fn t => subst_bounds (rev vs, t)) ts)) of
+      let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts in
+        (case Seq.pull (valid_conj ctxt facts empty_env
+            (map (fn t => subst_bounds (rev vs, t)) ts)) of
           SOME _ => true
-        | NONE => is_valid_disj ctxt facts ds
+        | NONE => is_valid_disj ctxt facts ds)
       end;
 
 val show_facts = Unsynchronized.ref false;
 
-fun string_of_facts ctxt s facts = space_implode "\n"
-  (s :: map (Syntax.string_of_term ctxt)
-     (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
+fun string_of_facts ctxt s facts =
+  space_implode "\n"
+    (s :: map (Syntax.string_of_term ctxt)
+      (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
 
 fun print_facts ctxt facts =
   if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts)
   else ();
 
 fun valid ctxt rules goal dom facts nfacts nparams =
-  let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
-    valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
-      let val cs' = map (fn (Ts, ts) =>
-        (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
-      in
-        inst_extra_vars ctxt dom cs' |>
-          Seq.map_filter (fn (inst, cs'') =>
-            if is_valid_disj ctxt facts cs'' then NONE
-            else SOME (th, env, inst, is, cs''))
-      end))
+  let
+    val seq =
+      Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
+        valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
+          let val cs' = map (fn (Ts, ts) =>
+            (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
+          in
+            inst_extra_vars ctxt dom cs' |>
+              Seq.map_filter (fn (inst, cs'') =>
+                if is_valid_disj ctxt facts cs'' then NONE
+                else SOME (th, env, inst, is, cs''))
+          end));
   in
-    case Seq.pull seq of
+    (case Seq.pull seq of
       NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE)
     | SOME ((th, env, inst, is, cs), _) =>
         if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
         else
           (case valid_cases ctxt rules goal dom facts nfacts nparams cs of
-             NONE => NONE
-           | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs)))
+            NONE => NONE
+          | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))))
   end
 
 and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME []
   | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
       let
         val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
-        val params = map_index (fn (i, T) =>
-          Free ("par" ^ string_of_int (nparams + i), T)) Ts;
-        val ts' = map_index (fn (i, t) =>
-          (subst_bounds (rev params, t), nfacts + i)) ts;
-        val dom' = fold (fn (T, p) =>
-          Typtab.map_default (T, []) (fn ps => ps @ [p]))
-            (Ts ~~ params) dom;
-        val facts' = fold (fn (t, i) => Net.insert_term op =
-          (t, (t, i))) ts' facts
+        val params = map_index (fn (i, T) => Free ("par" ^ string_of_int (nparams + i), T)) Ts;
+        val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts;
+        val dom' =
+          fold (fn (T, p) => Typtab.map_default (T, []) (fn ps => ps @ [p])) (Ts ~~ params) dom;
+        val facts' = fold (fn (t, i) => Net.insert_term op = (t, (t, i))) ts' facts;
       in
-        case valid ctxt rules goal dom' facts'
-          (nfacts + length ts) (nparams + length Ts) of
+        (case valid ctxt rules goal dom' facts' (nfacts + length ts) (nparams + length Ts) of
           NONE => NONE
-        | SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
-            NONE => NONE
-          | SOME prfs => SOME ((params, prf) :: prfs))
+        | SOME prf =>
+            (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
+              NONE => NONE
+            | SOME prfs => SOME ((params, prf) :: prfs)))
       end;
 
 
@@ -172,37 +174,41 @@
 
 fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
   let
-    val _ = message (fn () => space_implode "\n"
-      ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
-    val th' = Drule.implies_elim_list
-      (Thm.instantiate
-         (map (fn (ixn, (S, T)) =>
-            (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
-               (Vartab.dest tye),
-          map (fn (ixn, (T, t)) =>
-            (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
-             Thm.cterm_of thy t)) (Vartab.dest env) @
-          map (fn (ixnT, t) =>
-            (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
-      (map (nth asms) is);
-    val (_, cases) = dest_elim (prop_of th')
+    val _ =
+      message (fn () => space_implode "\n"
+        ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
+    val th' =
+      Drule.implies_elim_list
+        (Thm.instantiate
+           (map (fn (ixn, (S, T)) =>
+              (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
+                 (Vartab.dest tye),
+            map (fn (ixn, (T, t)) =>
+              (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
+               Thm.cterm_of thy t)) (Vartab.dest env) @
+            map (fn (ixnT, t) =>
+              (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
+        (map (nth asms) is);
+    val (_, cases) = dest_elim (prop_of th');
   in
-    case (cases, prfs) of
+    (case (cases, prfs) of
       ([([], [_])], []) => th'
     | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
-    | _ => Drule.implies_elim_list
-        (Thm.instantiate (Thm.match
-           (Drule.strip_imp_concl (cprop_of th'), goal)) th')
-        (map (thm_of_case_prf thy goal asms) (prfs ~~ cases))
+    | _ =>
+        Drule.implies_elim_list
+          (Thm.instantiate (Thm.match
+             (Drule.strip_imp_concl (cprop_of th'), goal)) th')
+          (map (thm_of_case_prf thy goal asms) (prfs ~~ cases)))
   end
 
 and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
   let
     val cparams = map (cterm_of thy) params;
-    val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms'
+    val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms';
   in
-    Drule.forall_intr_list cparams (Drule.implies_intr_list asms''
-      (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
+    Drule.forall_intr_list cparams
+      (Drule.implies_intr_list asms''
+        (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
   end;
 
 
@@ -211,15 +217,16 @@
 fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
   rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
   SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
-    let val xs = map (term_of o #2) params @
-      map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
-        (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
+    let
+      val xs =
+        map (term_of o #2) params @
+        map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
+          (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
     in
-      case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
+      (case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
            (mk_dom xs) Net.empty 0 0 of
-         NONE => no_tac
-       | SOME prf =>
-           rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1
+        NONE => no_tac
+      | SOME prf => rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1)
     end) ctxt' 1) ctxt;
 
 val setup = Method.setup @{binding coherent}
diff -r 0e2b7f04c944 -r 95c8ef02f04b src/Tools/cong_tac.ML
--- a/src/Tools/cong_tac.ML	Thu Feb 20 18:23:32 2014 +0100
+++ b/src/Tools/cong_tac.ML	Thu Feb 20 19:32:20 2014 +0100
@@ -21,14 +21,15 @@
       _ $ (_ $ (f $ x) $ (g $ y)) =>
         let
           val cong' = Thm.lift_rule cgoal cong;
-          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
-            Logic.strip_assums_concl (Thm.prop_of cong');
+          val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
           val ps = Logic.strip_params (Thm.concl_of cong');
-          val insts = [(f', f), (g', g), (x', x), (y', y)]
+          val insts =
+            [(f', f), (g', g), (x', x), (y', y)]
             |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
         in
-          fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
-            handle THM _ => no_tac st
+          fn st =>
+            compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
+              handle THM _ => no_tac st
         end
     | _ => no_tac)
   end);
diff -r 0e2b7f04c944 -r 95c8ef02f04b src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Thu Feb 20 18:23:32 2014 +0100
+++ b/src/Tools/intuitionistic.ML	Thu Feb 20 19:32:20 2014 +0100
@@ -42,17 +42,20 @@
   REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
   REMDUPS (unsafe_step_tac ctxt) i;
 
-fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
-  let
-    val ps = Logic.strip_assums_hyp g;
-    val c = Logic.strip_assums_concl g;
-  in
-    if member (fn ((ps1, c1), (ps2, c2)) =>
-        c1 aconv c2 andalso
-        length ps1 = length ps2 andalso
-        eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
-    else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
-  end);
+fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
+  if d > lim then no_tac
+  else
+    let
+      val ps = Logic.strip_assums_hyp g;
+      val c = Logic.strip_assums_concl g;
+    in
+      if member (fn ((ps1, c1), (ps2, c2)) =>
+          c1 aconv c2 andalso
+          length ps1 = length ps2 andalso
+          eq_set (op aconv) (ps1, ps2)) gs (ps, c)
+      then no_tac
+      else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
+    end);
 
 in
 
diff -r 0e2b7f04c944 -r 95c8ef02f04b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Feb 20 18:23:32 2014 +0100
+++ b/src/Tools/quickcheck.ML	Thu Feb 20 19:32:20 2014 +0100
@@ -83,11 +83,11 @@
 structure Quickcheck : QUICKCHECK =
 struct
 
-val quickcheckN = "quickcheck"
+val quickcheckN = "quickcheck";
 
-val genuineN = "genuine"
-val noneN = "none"
-val unknownN = "unknown"
+val genuineN = "genuine";
+val noneN = "none";
+val unknownN = "unknown";
 
 
 (* preferences *)
@@ -103,58 +103,63 @@
 (* quickcheck report *)
 
 datatype report = Report of
-  { iterations : int, raised_match_errors : int,
-    satisfied_assms : int list, positive_concl_tests : int }
+ {iterations : int,
+  raised_match_errors : int,
+  satisfied_assms : int list,
+  positive_concl_tests : int};
 
 
 (* Quickcheck Result *)
 
 datatype result = Result of
-  { counterexample : (bool * (string * term) list) option, evaluation_terms : (term * term) list option,
-    timings : (string * int) list, reports : (int * report) list}
+ {counterexample : (bool * (string * term) list) option,
+  evaluation_terms : (term * term) list option,
+  timings : (string * int) list,
+  reports : (int * report) list};
 
 val empty_result =
-  Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []}
+  Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []};
 
-fun counterexample_of (Result r) = #counterexample r
+fun counterexample_of (Result r) = #counterexample r;
 
-fun found_counterexample (Result r) = is_some (#counterexample r)
+fun found_counterexample (Result r) = is_some (#counterexample r);
 
-fun response_of (Result r) = case (#counterexample r, #evaluation_terms r) of
+fun response_of (Result r) =
+  (case (#counterexample r, #evaluation_terms r) of
     (SOME ts, SOME evals) => SOME (ts, evals)
-  | (NONE, NONE) => NONE
+  | (NONE, NONE) => NONE);
 
-fun timings_of (Result r) = #timings r
+fun timings_of (Result r) = #timings r;
 
 fun set_response names eval_terms (SOME (genuine, ts)) (Result r) =
-  let
-    val (ts1, ts2) = chop (length names) ts
-    val (eval_terms', _) = chop (length ts2) eval_terms
-  in
-    Result {counterexample = SOME (genuine, (names ~~ ts1)),
-      evaluation_terms = SOME (eval_terms' ~~ ts2),
-      timings = #timings r, reports = #reports r}
-  end
-  | set_response _ _ NONE result = result
+      let
+        val (ts1, ts2) = chop (length names) ts
+        val (eval_terms', _) = chop (length ts2) eval_terms
+      in
+        Result {counterexample = SOME (genuine, (names ~~ ts1)),
+          evaluation_terms = SOME (eval_terms' ~~ ts2),
+          timings = #timings r, reports = #reports r}
+      end
+  | set_response _ _ NONE result = result;
 
 
 fun cons_timing timing (Result r) =
   Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
-    timings = cons timing (#timings r), reports = #reports r}
+    timings = cons timing (#timings r), reports = #reports r};
 
 fun cons_report size (SOME report) (Result r) =
-  Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
-    timings = #timings r, reports = cons (size, report) (#reports r)}
-  | cons_report _ NONE result = result
+      Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
+        timings = #timings r, reports = cons (size, report) (#reports r)}
+  | cons_report _ NONE result = result;
 
 fun add_timing timing result_ref =
-  Unsynchronized.change result_ref (cons_timing timing)
+  Unsynchronized.change result_ref (cons_timing timing);
 
 fun add_report size report result_ref =
-  Unsynchronized.change result_ref (cons_report size report)
+  Unsynchronized.change result_ref (cons_report size report);
 
 fun add_response names eval_terms response result_ref =
-  Unsynchronized.change result_ref (set_response names eval_terms response)
+  Unsynchronized.change result_ref (set_response names eval_terms response);
 
 
 (* expectation *)
@@ -162,33 +167,33 @@
 datatype expectation = No_Expectation | No_Counterexample | Counterexample;
 
 fun merge_expectation (expect1, expect2) =
-  if expect1 = expect2 then expect1 else No_Expectation
+  if expect1 = expect2 then expect1 else No_Expectation;
 
 (*quickcheck configuration -- default parameters, test generators*)
-val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "")
-val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
-val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
-val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10)
+val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "");
+val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10);
+val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100);
+val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10);
 
-val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
-val locale = Attrib.setup_config_string @{binding quickcheck_locale} (K "interpret expand")
-val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
-val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
-val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false);
+val locale = Attrib.setup_config_string @{binding quickcheck_locale} (K "interpret expand");
+val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true);
+val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false);
+val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0);
 
-val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
-val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
+val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false);
+val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false);
 
-val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
-val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
-val tag = Attrib.setup_config_string @{binding quickcheck_tag} (K "")
+val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false);
+val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false);
+val tag = Attrib.setup_config_string @{binding quickcheck_tag} (K "");
 
-val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false)
+val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false);
 
 val allow_function_inversion =
-  Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
-val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
-val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3)
+  Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false);
+val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true);
+val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3);
 
 datatype test_params = Test_Params of
   {default_type: typ list, expect : expectation};
@@ -213,13 +218,14 @@
 structure Data = Generic_Data
 (
   type T =
-    ((string * (bool Config.T * tester)) list
-      * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
-      * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
-      * test_params;
+    ((string * (bool Config.T * tester)) list *
+      ((string * (Proof.context -> term list -> (int -> term list option) list)) list *
+      ((string * (Proof.context -> term list -> (int -> bool) list)) list))) *
+      test_params;
   val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
   val extend = I;
-  fun merge (((testers1, (batch_generators1, batch_validators1)), params1),
+  fun merge
+   (((testers1, (batch_generators1, batch_validators1)), params1),
     ((testers2, (batch_generators2, batch_validators2)), params2)) : T =
     ((AList.merge (op =) (K true) (testers1, testers2),
       (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
@@ -229,11 +235,11 @@
 
 val test_params_of = snd o Data.get o Context.Proof;
 
-val default_type = fst o dest_test_params o test_params_of
+val default_type = fst o dest_test_params o test_params_of;
 
-val expect = snd o dest_test_params o test_params_of
+val expect = snd o dest_test_params o test_params_of;
 
-val map_test_params = Data.map o apsnd o map_test_params'
+val map_test_params = Data.map o apsnd o map_test_params';
 
 val add_tester = Data.map o apfst o apfst o AList.update (op =);
 
@@ -243,15 +249,15 @@
 
 fun active_testers ctxt =
   let
-    val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt
+    val testers = map snd (fst (fst (Data.get (Context.Proof ctxt))));
   in
     map snd (filter (fn (active, _) => Config.get ctxt active) testers)
-  end
+  end;
 
 fun set_active_testers [] gen_ctxt = gen_ctxt
   | set_active_testers testers gen_ctxt =
       let
-        val registered_testers = (fst o fst o Data.get) gen_ctxt
+        val registered_testers = fst (fst (Data.get gen_ctxt));
       in
         fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
           registered_testers gen_ctxt
@@ -281,9 +287,9 @@
   end;
 
 val mk_batch_tester =
-  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt));
+  gen_mk_tester (AList.lookup (op =) o fst o snd o fst o Data.get o Context.Proof);
 val mk_batch_validator =
-  gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt));
+  gen_mk_tester (AList.lookup (op =) o snd o snd o fst o Data.get o Context.Proof);
 
 
 (* testing propositions *)
@@ -293,11 +299,10 @@
 
 fun limit timeout (limit_time, is_interactive) f exc () =
   if limit_time then
-      TimeLimit.timeLimit timeout f ()
-    handle TimeLimit.TimeOut =>
-      if is_interactive then exc () else raise TimeLimit.TimeOut
-  else
-    f ();
+    TimeLimit.timeLimit timeout f ()
+      handle TimeLimit.TimeOut =>
+        if is_interactive then exc () else raise TimeLimit.TimeOut
+  else f ();
 
 fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s;
 
@@ -309,11 +314,13 @@
   (case active_testers ctxt of
     [] => error "No active testers for quickcheck"
   | testers =>
-    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
-      (fn () => Par_List.get_some (fn tester =>
-        tester ctxt (length testers > 1) insts goals |>
-        (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
-      (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ());
+      limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
+        (fn () =>
+          Par_List.get_some (fn tester =>
+            tester ctxt (length testers > 1) insts goals |>
+            (fn result => if exists found_counterexample result then SOME result else NONE))
+          testers)
+        (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ());
 
 fun all_axioms_of ctxt t =
   let
@@ -341,7 +348,8 @@
     val cs = space_explode " " s;
   in
     if forall (fn c => c = "expand" orelse c = "interpret") cs then cs
-    else (warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
+    else
+     (warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
       ["interpret", "expand"])
   end;
 
@@ -370,18 +378,19 @@
       (case fst (Locale.specification_of thy locale) of
         NONE => []
       | SOME t => the_default [] (all_axioms_of lthy t));
-   val config = locale_config_of (Config.get lthy locale);
-   val goals =
-    (case some_locale of
-      NONE => [(proto_goal, eval_terms)]
-    | SOME locale =>
-        fold (fn c =>
-          if c = "expand" then cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms)
-          else if c = "interpret" then
-            append (map (fn (_, phi) =>
-                (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
-              (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale))
-          else I) config []);
+    val config = locale_config_of (Config.get lthy locale);
+    val goals =
+      (case some_locale of
+        NONE => [(proto_goal, eval_terms)]
+      | SOME locale =>
+          fold (fn c =>
+            if c = "expand" then
+              cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms)
+            else if c = "interpret" then
+              append (map (fn (_, phi) =>
+                  (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
+                (Locale.registrations_of (Context.Theory thy) (* FIXME !? *) locale))
+            else I) config []);
     val _ =
       verbose_message lthy
         (Pretty.string_of
@@ -396,39 +405,39 @@
 fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck";
 
 fun pretty_counterex ctxt auto NONE =
-    Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
+      Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
   | pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) =
       (Pretty.text_fold o Pretty.fbreaks)
-        (Pretty.str (tool_name auto ^ " found a " ^
+       (Pretty.str (tool_name auto ^ " found a " ^
          (if genuine then "counterexample:"
           else "potentially spurious counterexample due to underspecified functions:") ^
-         Config.get ctxt tag) ::
-         Pretty.str "" ::
-         map (fn (s, t) =>
+        Config.get ctxt tag) ::
+        Pretty.str "" ::
+        map (fn (s, t) =>
           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex) @
-         (if null eval_terms then []
-          else
-           Pretty.str "" :: Pretty.str "Evaluated terms:" ::
-           map (fn (t, u) =>
-            Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
-             Syntax.pretty_term ctxt u]) (rev eval_terms)));
+        (if null eval_terms then []
+         else
+          Pretty.str "" :: Pretty.str "Evaluated terms:" ::
+            map (fn (t, u) =>
+              Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
+                Syntax.pretty_term ctxt u]) (rev eval_terms)));
 
 
 (* Isar commands *)
 
 fun read_nat s =
-  (case (Library.read_int o Symbol.explode) s of
+  (case Library.read_int (Symbol.explode s) of
     (k, []) =>
       if k >= 0 then k
       else error ("Not a natural number: " ^ s)
-  | (_, _ :: _) => error ("Not a natural number: " ^ s));
+  | _ => error ("Not a natural number: " ^ s));
 
 fun read_bool "false" = false
   | read_bool "true" = true
   | read_bool s = error ("Not a Boolean value: " ^ s);
 
 fun read_real s =
-  (case (Real.fromString s) of
+  (case Real.fromString s of
     SOME s => s
   | NONE => error ("Not a real number: " ^ s));
 
@@ -437,36 +446,42 @@
   | read_expectation "counterexample" = Counterexample
   | read_expectation s = error ("Not an expectation value: " ^ s);
 
-fun valid_tester_name genctxt name = AList.defined (op =) (fst (fst (Data.get genctxt))) name;
+fun valid_tester_name genctxt name =
+  AList.defined (op =) (fst (fst (Data.get genctxt))) name;
 
 fun parse_tester name (testers, genctxt) =
   if valid_tester_name genctxt name then
     (insert (op =) name testers, genctxt)
-  else
-    error ("Unknown tester: " ^ name);
+  else error ("Unknown tester: " ^ name);
 
 fun parse_test_param ("tester", args) = fold parse_tester args
   | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg))
   | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
   | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg))
-  | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) =>
-    (testers, map_test_params
-      ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))
+  | parse_test_param ("default_type", arg) =
+      (fn (testers, gen_ctxt) =>
+        (testers, map_test_params
+          (apfst (K (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg))) gen_ctxt))
   | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
-  | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
+  | parse_test_param ("expect", [arg]) = apsnd (map_test_params (apsnd (K (read_expectation arg))))
   | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
-  | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
-  | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
+  | parse_test_param ("genuine_only", [arg]) =
+      apsnd (Config.put_generic genuine_only (read_bool arg))
+  | parse_test_param ("abort_potential", [arg]) =
+      apsnd (Config.put_generic abort_potential (read_bool arg))
   | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
   | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
   | parse_test_param ("tag", [arg]) = apsnd (Config.put_generic tag arg)
-  | parse_test_param ("use_subtype", [arg]) = apsnd (Config.put_generic use_subtype (read_bool arg))
-  | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
-  | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
+  | parse_test_param ("use_subtype", [arg]) =
+      apsnd (Config.put_generic use_subtype (read_bool arg))
+  | parse_test_param ("timeout", [arg]) =
+      apsnd (Config.put_generic timeout (read_real arg))
+  | parse_test_param ("finite_types", [arg]) =
+      apsnd (Config.put_generic finite_types (read_bool arg))
   | parse_test_param ("allow_function_inversion", [arg]) =
       apsnd (Config.put_generic allow_function_inversion (read_bool arg))
   | parse_test_param ("finite_type_size", [arg]) =
-    apsnd (Config.put_generic finite_type_size (read_nat arg))
+      apsnd (Config.put_generic finite_type_size (read_nat arg))
   | parse_test_param (name, _) =
       (fn (testers, genctxt) =>
         if valid_tester_name genctxt name then
@@ -487,8 +502,9 @@
         ((insts, eval_terms),
           proof_map_result (fn gen_ctxt => parse_test_param (name, arg) (testers, gen_ctxt)) ctxt)));
 
-fun quickcheck_params_cmd args = Context.theory_map
-  (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
+fun quickcheck_params_cmd args =
+  Context.theory_map
+    (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
 
 fun check_expectation state results =
   if is_some results andalso expect (Proof.context_of state) = No_Counterexample then
@@ -502,8 +518,10 @@
   |> Proof.map_context_result (fn ctxt =>
     apsnd (fn (testers, ctxt) => Context.proof_map (set_active_testers testers) ctxt)
       (fold parse_test_param_inst args (([], []), ([], ctxt))))
-  |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state'
-      |> tap (check_expectation state') |> rpair state');
+  |> (fn ((insts, eval_terms), state') =>
+      test_goal (true, true) (insts, eval_terms) i state'
+      |> tap (check_expectation state')
+      |> rpair state');
 
 fun quickcheck args i state =
   Option.map (the o get_first counterexample_of) (fst (gen_quickcheck args i state));