tuning
authorblanchet
Mon Feb 03 15:33:18 2014 +0100 (2014-02-03 ago)
changeset 552867bbbd9393ce0
parent 55285 e88ad20035f4
child 55287 ffa306239316
tuning
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Feb 03 15:19:07 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Feb 03 15:33:18 2014 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4  open ATP_Problem_Generate
     1.5  open Sledgehammer_Util
     1.6  open Sledgehammer_Fact
     1.7 +open Sledgehammer_Reconstructor
     1.8  open Sledgehammer_Prover
     1.9  open Sledgehammer_Prover_ATP
    1.10  open Sledgehammer_Prover_Minimize
    1.11 @@ -49,13 +50,11 @@
    1.12    NONE
    1.13    |> fold (fn candidate =>
    1.14                fn accum as SOME _ => accum
    1.15 -               | NONE => if member (op =) codes candidate then SOME candidate
    1.16 -                         else NONE)
    1.17 -          ordered_outcome_codes
    1.18 +               | NONE => if member (op =) codes candidate then SOME candidate else NONE)
    1.19 +       ordered_outcome_codes
    1.20    |> the_default unknownN
    1.21  
    1.22 -fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
    1.23 -                       n goal =
    1.24 +fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal =
    1.25    (quote name,
    1.26     (if verbose then
    1.27        " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    1.28 @@ -211,88 +210,91 @@
    1.29  fun string_of_factss factss =
    1.30    if forall (null o snd) factss then
    1.31      "Found no relevant facts."
    1.32 -  else case factss of
    1.33 -    [(_, facts)] => string_of_facts facts
    1.34 -  | _ =>
    1.35 -    factss
    1.36 -    |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
    1.37 -    |> space_implode "\n\n"
    1.38 +  else
    1.39 +    (case factss of
    1.40 +      [(_, facts)] => string_of_facts facts
    1.41 +    | _ =>
    1.42 +      factss
    1.43 +      |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
    1.44 +      |> space_implode "\n\n")
    1.45  
    1.46  fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode
    1.47      output_result i (fact_override as {only, ...}) minimize_command state =
    1.48    if null provers then
    1.49      error "No prover is set."
    1.50 -  else case subgoal_count state of
    1.51 -    0 =>
    1.52 +  else
    1.53 +    (case subgoal_count state of
    1.54 +      0 =>
    1.55        ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
    1.56 -  | n =>
    1.57 -    let
    1.58 -      val _ = Proof.assert_backward state
    1.59 -      val print =
    1.60 -        if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
    1.61 -      val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug)
    1.62 -      val ctxt = Proof.context_of state
    1.63 -      val {facts = chained, goal, ...} = Proof.goal state
    1.64 -      val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
    1.65 -      val ho_atp = exists (is_ho_atp ctxt) provers
    1.66 -      val reserved = reserved_isar_keyword_table ()
    1.67 -      val css = clasimpset_rule_table_of ctxt
    1.68 -      val all_facts =
    1.69 -        nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
    1.70 -                         concl_t
    1.71 -      val _ = () |> not blocking ? kill_provers
    1.72 -      val _ = case find_first (not o is_prover_supported ctxt) provers of
    1.73 -                SOME name => error ("No such prover: " ^ name ^ ".")
    1.74 -              | NONE => ()
    1.75 -      val _ = print "Sledgehammering..."
    1.76 -      val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
    1.77 +    | n =>
    1.78 +      let
    1.79 +        val _ = Proof.assert_backward state
    1.80 +        val print =
    1.81 +          if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
    1.82 +        val state = state |> Proof.map_context (silence_proof_methods debug)
    1.83 +        val ctxt = Proof.context_of state
    1.84 +        val {facts = chained, goal, ...} = Proof.goal state
    1.85 +        val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
    1.86 +        val ho_atp = exists (is_ho_atp ctxt) provers
    1.87 +        val reserved = reserved_isar_keyword_table ()
    1.88 +        val css = clasimpset_rule_table_of ctxt
    1.89 +        val all_facts =
    1.90 +          nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
    1.91 +                           concl_t
    1.92 +        val _ = () |> not blocking ? kill_provers
    1.93 +        val _ =
    1.94 +          (case find_first (not o is_prover_supported ctxt) provers of
    1.95 +            SOME name => error ("No such prover: " ^ name ^ ".")
    1.96 +          | NONE => ())
    1.97 +        val _ = print "Sledgehammering..."
    1.98 +        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
    1.99  
   1.100 -      val spying_str_of_factss =
   1.101 -        commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
   1.102 +        val spying_str_of_factss =
   1.103 +          commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
   1.104  
   1.105 -      fun get_factss provers =
   1.106 -        let
   1.107 -          val max_max_facts =
   1.108 -            case max_facts of
   1.109 -              SOME n => n
   1.110 -            | NONE =>
   1.111 -              0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
   1.112 -                |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
   1.113 -          val _ = spying spy (fn () => (state, i, "All",
   1.114 -            "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
   1.115 -        in
   1.116 -          all_facts
   1.117 -          |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
   1.118 -          |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
   1.119 -          |> spy ? tap (fn factss => spying spy (fn () =>
   1.120 -            (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
   1.121 -        end
   1.122 +        fun get_factss provers =
   1.123 +          let
   1.124 +            val max_max_facts =
   1.125 +              (case max_facts of
   1.126 +                SOME n => n
   1.127 +              | NONE =>
   1.128 +                0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
   1.129 +                  |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
   1.130 +            val _ = spying spy (fn () => (state, i, "All",
   1.131 +              "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
   1.132 +          in
   1.133 +            all_facts
   1.134 +            |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
   1.135 +            |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
   1.136 +            |> spy ? tap (fn factss => spying spy (fn () =>
   1.137 +              (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
   1.138 +          end
   1.139  
   1.140 -      fun launch_provers state =
   1.141 -        let
   1.142 -          val factss = get_factss provers
   1.143 -          val problem =
   1.144 -            {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
   1.145 -             factss = factss}
   1.146 -          val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
   1.147 -          val launch = launch_prover params mode output_result minimize_command only learn
   1.148 -        in
   1.149 -          if mode = Auto_Try then
   1.150 -            (unknownN, state)
   1.151 -            |> fold (fn prover => fn accum as (outcome_code, _) =>
   1.152 -                        if outcome_code = someN then accum
   1.153 -                        else launch problem prover)
   1.154 -                    provers
   1.155 -          else
   1.156 -            provers
   1.157 -            |> (if blocking then Par_List.map else map) (launch problem #> fst)
   1.158 -            |> max_outcome_code |> rpair state
   1.159 -        end
   1.160 -    in
   1.161 -      (if blocking then launch_provers state
   1.162 -       else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
   1.163 -      handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
   1.164 -    end
   1.165 -    |> `(fn (outcome_code, _) => outcome_code = someN)
   1.166 +        fun launch_provers state =
   1.167 +          let
   1.168 +            val factss = get_factss provers
   1.169 +            val problem =
   1.170 +              {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
   1.171 +               factss = factss}
   1.172 +            val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
   1.173 +            val launch = launch_prover params mode output_result minimize_command only learn
   1.174 +          in
   1.175 +            if mode = Auto_Try then
   1.176 +              (unknownN, state)
   1.177 +              |> fold (fn prover => fn accum as (outcome_code, _) =>
   1.178 +                          if outcome_code = someN then accum
   1.179 +                          else launch problem prover)
   1.180 +                      provers
   1.181 +            else
   1.182 +              provers
   1.183 +              |> (if blocking then Par_List.map else map) (launch problem #> fst)
   1.184 +              |> max_outcome_code |> rpair state
   1.185 +          end
   1.186 +      in
   1.187 +        (if blocking then launch_provers state
   1.188 +         else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
   1.189 +        handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
   1.190 +      end
   1.191 +      |> `(fn (outcome_code, _) => outcome_code = someN))
   1.192  
   1.193  end;
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 15:19:07 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 15:33:18 2014 +0100
     2.3 @@ -131,12 +131,12 @@
     2.4    member (op =) property_dependent_params s orelse s = "expect"
     2.5  
     2.6  fun is_prover_list ctxt s =
     2.7 -  case space_explode " " s of
     2.8 +  (case space_explode " " s of
     2.9      ss as _ :: _ => forall (is_prover_supported ctxt) ss
    2.10 -  | _ => false
    2.11 +  | _ => false)
    2.12  
    2.13  fun unalias_raw_param (name, value) =
    2.14 -  case AList.lookup (op =) alias_params name of
    2.15 +  (case AList.lookup (op =) alias_params name of
    2.16      SOME (name', []) => (name', value)
    2.17    | SOME (param' as (name', _)) =>
    2.18      if value <> ["false"] then
    2.19 @@ -145,13 +145,14 @@
    2.20        error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
    2.21               \(cf. " ^ quote name' ^ ").")
    2.22    | NONE =>
    2.23 -    case AList.lookup (op =) negated_alias_params name of
    2.24 -      SOME name' => (name', case value of
    2.25 -                              ["false"] => ["true"]
    2.26 -                            | ["true"] => ["false"]
    2.27 -                            | [] => ["false"]
    2.28 -                            | _ => value)
    2.29 -    | NONE => (name, value)
    2.30 +    (case AList.lookup (op =) negated_alias_params name of
    2.31 +      SOME name' => (name',
    2.32 +        (case value of
    2.33 +          ["false"] => ["true"]
    2.34 +        | ["true"] => ["false"]
    2.35 +        | [] => ["false"]
    2.36 +        | _ => value))
    2.37 +    | NONE => (name, value)))
    2.38  
    2.39  val any_type_enc = type_enc_of_string Strict "erased"
    2.40  
    2.41 @@ -266,9 +267,10 @@
    2.42      val type_enc =
    2.43        if mode = Auto_Try then
    2.44          NONE
    2.45 -      else case lookup_string "type_enc" of
    2.46 -        "smart" => NONE
    2.47 -      | s => (type_enc_of_string Strict s; SOME s)
    2.48 +      else
    2.49 +        (case lookup_string "type_enc" of
    2.50 +          "smart" => NONE
    2.51 +        | s => (type_enc_of_string Strict s; SOME s))
    2.52      val strict = mode = Auto_Try orelse lookup_bool "strict"
    2.53      val lam_trans = lookup_option lookup_string "lam_trans"
    2.54      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Feb 03 15:19:07 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Feb 03 15:33:18 2014 +0100
     3.3 @@ -110,18 +110,18 @@
     3.4      fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
     3.5        | normT (TVar (z as (_, S))) =
     3.6          (fn ((knownT, nT), accum) =>
     3.7 -            case find_index (equal z) knownT of
     3.8 +            (case find_index (equal z) knownT of
     3.9                ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
    3.10 -            | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))
    3.11 +            | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))))
    3.12        | normT (T as TFree _) = pair T
    3.13      fun norm (t $ u) = norm t ##>> norm u #>> op $
    3.14        | norm (Const (s, T)) = normT T #>> curry Const s
    3.15        | norm (Var (z as (_, T))) =
    3.16          normT T
    3.17          #> (fn (T, (accumT, (known, n))) =>
    3.18 -               case find_index (equal z) known of
    3.19 +               (case find_index (equal z) known of
    3.20                   ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
    3.21 -               | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))
    3.22 +               | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n)))))
    3.23        | norm (Abs (_, T, t)) =
    3.24          norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
    3.25        | norm (Bound j) = pair (Bound j)
    3.26 @@ -138,11 +138,11 @@
    3.27          Induction
    3.28        else
    3.29          let val t = normalize_vars t in
    3.30 -          case Termtab.lookup css t of
    3.31 +          (case Termtab.lookup css t of
    3.32              SOME status => status
    3.33            | NONE =>
    3.34              let val concl = Logic.strip_imp_concl t in
    3.35 -              case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
    3.36 +              (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
    3.37                  SOME lrhss =>
    3.38                  let
    3.39                    val prems = Logic.strip_imp_prems t
    3.40 @@ -150,8 +150,8 @@
    3.41                  in
    3.42                    Termtab.lookup css t' |> the_default General
    3.43                  end
    3.44 -              | NONE => General
    3.45 -            end
    3.46 +              | NONE => General)
    3.47 +            end)
    3.48          end
    3.49      end
    3.50  
    3.51 @@ -165,15 +165,14 @@
    3.52        map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
    3.53        |> implode
    3.54      fun nth_name j =
    3.55 -      case xref of
    3.56 +      (case xref of
    3.57          Facts.Fact s => backquote s ^ bracket
    3.58        | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
    3.59        | Facts.Named ((name, _), NONE) =>
    3.60          make_name reserved (length ths > 1) (j + 1) name ^ bracket
    3.61        | Facts.Named ((name, _), SOME intervals) =>
    3.62          make_name reserved true
    3.63 -                 (nth (maps (explode_interval (length ths)) intervals) j) name ^
    3.64 -        bracket
    3.65 +          (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
    3.66      fun add_nth th (j, rest) =
    3.67        let val name = nth_name j in
    3.68          (j + 1, ((name, stature_of_thm false [] chained css name th), th)
    3.69 @@ -364,9 +363,9 @@
    3.70     corresponding low-level facts, so that MaSh can learn from the low-level
    3.71     proofs. *)
    3.72  fun un_class_ify s =
    3.73 -  case first_field "_class" s of
    3.74 +  (case first_field "_class" s of
    3.75      SOME (pref, suf) => [s, pref ^ suf]
    3.76 -  | NONE => [s]
    3.77 +  | NONE => [s])
    3.78  
    3.79  fun build_name_tables name_of facts =
    3.80    let
    3.81 @@ -388,7 +387,7 @@
    3.82    |> Net.entries
    3.83  
    3.84  fun struct_induct_rule_on th =
    3.85 -  case Logic.strip_horn (prop_of th) of
    3.86 +  (case Logic.strip_horn (prop_of th) of
    3.87      (prems, @{const Trueprop}
    3.88              $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
    3.89      if not (is_TVar ind_T) andalso length prems > 1 andalso
    3.90 @@ -397,7 +396,7 @@
    3.91        SOME (p_name, ind_T)
    3.92      else
    3.93        NONE
    3.94 -  | _ => NONE
    3.95 +  | _ => NONE)
    3.96  
    3.97  val instantiate_induct_timeout = seconds 0.01
    3.98  
    3.99 @@ -420,14 +419,15 @@
   3.100    handle Type.TYPE_MATCH => false
   3.101  
   3.102  fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
   3.103 -  case struct_induct_rule_on th of
   3.104 +  (case struct_induct_rule_on th of
   3.105      SOME (p_name, ind_T) =>
   3.106      let val thy = Proof_Context.theory_of ctxt in
   3.107 -      stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
   3.108 -              |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
   3.109 -                     (instantiate_induct_rule ctxt stmt p_name ax)))
   3.110 +      stmt_xs
   3.111 +      |> filter (fn (_, T) => type_match thy (T, ind_T))
   3.112 +      |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
   3.113 +           (instantiate_induct_rule ctxt stmt p_name ax)))
   3.114      end
   3.115 -  | NONE => [ax]
   3.116 +  | NONE => [ax])
   3.117  
   3.118  fun external_frees t =
   3.119    [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   3.120 @@ -482,9 +482,9 @@
   3.121              val n = length ths
   3.122              val multi = n > 1
   3.123              fun check_thms a =
   3.124 -              case try (Proof_Context.get_thms ctxt) a of
   3.125 +              (case try (Proof_Context.get_thms ctxt) a of
   3.126                  NONE => false
   3.127 -              | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   3.128 +              | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths'))
   3.129            in
   3.130              snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_accum)) =>
   3.131                (j - 1,
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 15:19:07 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 15:33:18 2014 +0100
     4.3 @@ -284,9 +284,7 @@
     4.4            |> postprocess_isar_proof_remove_unreferenced_steps I
     4.5            |> relabel_isar_proof_canonically
     4.6  
     4.7 -        val ctxt = ctxt
     4.8 -          |> enrich_context_with_local_facts canonical_isar_proof
     4.9 -          |> silence_proof_methods debug
    4.10 +        val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
    4.11  
    4.12          val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
    4.13  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Mon Feb 03 15:19:07 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Mon Feb 03 15:33:18 2014 +0100
     5.3 @@ -41,12 +41,12 @@
     5.4    post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
     5.5  
     5.6  fun fold_map_atypes f T s =
     5.7 -  case T of
     5.8 +  (case T of
     5.9      Type (name, Ts) =>
    5.10 -        let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
    5.11 -          (Type (name, Ts), s)
    5.12 -        end
    5.13 -  | _ => f T s
    5.14 +    let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
    5.15 +      (Type (name, Ts), s)
    5.16 +    end
    5.17 +  | _ => f T s)
    5.18  
    5.19  val indexname_ord = Term_Ord.fast_indexname_ord
    5.20  val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 03 15:19:07 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 03 15:33:18 2014 +0100
     6.3 @@ -178,9 +178,9 @@
     6.4      fun run_on () =
     6.5        (Isabelle_System.bash command
     6.6         |> tap (fn _ =>
     6.7 -            case try File.read (Path.explode err_file) |> the_default "" of
     6.8 +            (case try File.read (Path.explode err_file) |> the_default "" of
     6.9                "" => trace_msg ctxt (K "Done")
    6.10 -            | s => warning ("MaSh error: " ^ elide_string 1000 s));
    6.11 +            | s => warning ("MaSh error: " ^ elide_string 1000 s)));
    6.12         read_suggs (fn () => try File.read_lines sugg_path |> these))
    6.13      fun clean_up () =
    6.14        if overlord then ()
    6.15 @@ -243,17 +243,16 @@
    6.16  
    6.17  (* The suggested weights don't make much sense. *)
    6.18  fun extract_suggestion sugg =
    6.19 -  case space_explode "=" sugg of
    6.20 +  (case space_explode "=" sugg of
    6.21      [name, _ (* weight *)] =>
    6.22      SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *))
    6.23    | [name] => SOME (unencode_str name (* , 1.0 *))
    6.24 -  | _ => NONE
    6.25 +  | _ => NONE)
    6.26  
    6.27  fun extract_suggestions line =
    6.28 -  case space_explode ":" line of
    6.29 -    [goal, suggs] =>
    6.30 -    (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
    6.31 -  | _ => ("", [])
    6.32 +  (case space_explode ":" line of
    6.33 +    [goal, suggs] => (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
    6.34 +  | _ => ("", []))
    6.35  
    6.36  structure MaSh =
    6.37  struct
    6.38 @@ -294,11 +293,10 @@
    6.39  
    6.40  fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
    6.41    (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
    6.42 -   run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs)
    6.43 -       (fn suggs =>
    6.44 -           case suggs () of
    6.45 -             [] => []
    6.46 -           | suggs => snd (extract_suggestions (List.last suggs)))
    6.47 +   run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs =>
    6.48 +     (case suggs () of
    6.49 +       [] => []
    6.50 +     | suggs => snd (extract_suggestions (List.last suggs))))
    6.51     handle List.Empty => [])
    6.52  
    6.53  end;
    6.54 @@ -362,48 +360,47 @@
    6.55  exception FILE_VERSION_TOO_NEW of unit
    6.56  
    6.57  fun extract_node line =
    6.58 -  case space_explode ":" line of
    6.59 +  (case space_explode ":" line of
    6.60      [head, parents] =>
    6.61      (case space_explode " " head of
    6.62 -       [kind, name] =>
    6.63 -       SOME (unencode_str name, unencode_strs parents,
    6.64 -             try proof_kind_of_str kind |> the_default Isar_Proof)
    6.65 -     | _ => NONE)
    6.66 -  | _ => NONE
    6.67 +      [kind, name] =>
    6.68 +      SOME (unencode_str name, unencode_strs parents,
    6.69 +        try proof_kind_of_str kind |> the_default Isar_Proof)
    6.70 +    | _ => NONE)
    6.71 +  | _ => NONE)
    6.72  
    6.73  fun load_state _ _ (state as (true, _)) = state
    6.74    | load_state ctxt overlord _ =
    6.75      let val path = mash_state_file () in
    6.76        (true,
    6.77 -       case try File.read_lines path of
    6.78 +       (case try File.read_lines path of
    6.79           SOME (version' :: node_lines) =>
    6.80           let
    6.81             fun add_edge_to name parent =
    6.82               Graph.default_node (parent, Isar_Proof)
    6.83               #> Graph.add_edge (parent, name)
    6.84             fun add_node line =
    6.85 -             case extract_node line of
    6.86 +             (case extract_node line of
    6.87                 NONE => I (* shouldn't happen *)
    6.88               | SOME (name, parents, kind) =>
    6.89 -               update_access_graph_node (name, kind)
    6.90 -               #> fold (add_edge_to name) parents
    6.91 +               update_access_graph_node (name, kind) #> fold (add_edge_to name) parents)
    6.92             val (access_G, num_known_facts) =
    6.93 -             case string_ord (version', version) of
    6.94 +             (case string_ord (version', version) of
    6.95                 EQUAL =>
    6.96                 (try_graph ctxt "loading state" Graph.empty (fn () =>
    6.97 -                    fold add_node node_lines Graph.empty),
    6.98 +                  fold add_node node_lines Graph.empty),
    6.99                  length node_lines)
   6.100               | LESS =>
   6.101                 (* can't parse old file *)
   6.102                 (MaSh.unlearn ctxt overlord; (Graph.empty, 0))
   6.103 -             | GREATER => raise FILE_VERSION_TOO_NEW ()
   6.104 +             | GREATER => raise FILE_VERSION_TOO_NEW ())
   6.105           in
   6.106             trace_msg ctxt (fn () =>
   6.107                 "Loaded fact graph (" ^ graph_info access_G ^ ")");
   6.108             {access_G = access_G, num_known_facts = num_known_facts,
   6.109              dirty = SOME []}
   6.110           end
   6.111 -       | _ => empty_state)
   6.112 +       | _ => empty_state))
   6.113      end
   6.114  
   6.115  fun save_state _ (state as {dirty = SOME [], ...}) = state
   6.116 @@ -415,10 +412,9 @@
   6.117        fun append_entry (name, (kind, (parents, _))) =
   6.118          cons (name, Graph.Keys.dest parents, kind)
   6.119        val (banner, entries) =
   6.120 -        case dirty of
   6.121 -          SOME names =>
   6.122 -          (NONE, fold (append_entry o Graph.get_entry access_G) names [])
   6.123 -        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])
   6.124 +        (case dirty of
   6.125 +          SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
   6.126 +        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []))
   6.127      in
   6.128        write_file banner (entries, str_of_entry) (mash_state_file ());
   6.129        trace_msg ctxt (fn () =>
   6.130 @@ -471,11 +467,11 @@
   6.131    if Thm.has_name_hint th then
   6.132      let val hint = Thm.get_name_hint th in
   6.133        (* There must be a better way to detect local facts. *)
   6.134 -      case try (unprefix local_prefix) hint of
   6.135 +      (case try (unprefix local_prefix) hint of
   6.136          SOME suf =>
   6.137 -        thy_name_of_thm th ^ Long_Name.separator ^ suf ^
   6.138 -        Long_Name.separator ^ elided_backquote_thm 50 th
   6.139 -      | NONE => hint
   6.140 +        thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
   6.141 +        elided_backquote_thm 50 th
   6.142 +      | NONE => hint)
   6.143      end
   6.144    else
   6.145      elided_backquote_thm 200 th
   6.146 @@ -512,9 +508,9 @@
   6.147          let
   6.148            val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score)
   6.149          in
   6.150 -          case find_index (curry fact_eq fact o fst) sels of
   6.151 +          (case find_index (curry fact_eq fact o fst) sels of
   6.152              ~1 => if member fact_eq unks fact then NONE else SOME 0.0
   6.153 -          | rank => score_at rank
   6.154 +          | rank => score_at rank)
   6.155          end
   6.156        fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
   6.157        val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
   6.158 @@ -536,20 +532,21 @@
   6.159      if Theory.eq_thy p then EQUAL else LESS
   6.160    else if Theory.subthy (swap p) then
   6.161      GREATER
   6.162 -  else case int_ord (pairself (length o Theory.ancestors_of) p) of
   6.163 -    EQUAL => string_ord (pairself Context.theory_name p)
   6.164 -  | order => order
   6.165 +  else
   6.166 +    (case int_ord (pairself (length o Theory.ancestors_of) p) of
   6.167 +      EQUAL => string_ord (pairself Context.theory_name p)
   6.168 +    | order => order)
   6.169  
   6.170  fun crude_thm_ord p =
   6.171 -  case crude_theory_ord (pairself theory_of_thm p) of
   6.172 +  (case crude_theory_ord (pairself theory_of_thm p) of
   6.173      EQUAL =>
   6.174      let val q = pairself nickname_of_thm p in
   6.175        (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
   6.176 -      case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
   6.177 +      (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
   6.178          EQUAL => string_ord q
   6.179 -      | ord => ord
   6.180 +      | ord => ord)
   6.181      end
   6.182 -  | ord => ord
   6.183 +  | ord => ord)
   6.184  
   6.185  val thm_less_eq = Theory.subthy o pairself theory_of_thm
   6.186  fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
   6.187 @@ -724,7 +721,7 @@
   6.188          add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
   6.189      fun add_term Ts = add_term_pats Ts term_max_depth
   6.190      fun add_subterms Ts t =
   6.191 -      case strip_comb t of
   6.192 +      (case strip_comb t of
   6.193          (Const (s, T), args) =>
   6.194          (not (is_widely_irrelevant_const s) ? add_term Ts t)
   6.195          #> add_subtypes T
   6.196 @@ -735,7 +732,7 @@
   6.197           | Var (_, T) => add_subtypes T
   6.198           | Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body
   6.199           | _ => I)
   6.200 -        #> fold (add_subterms Ts) args
   6.201 +        #> fold (add_subterms Ts) args)
   6.202    in [] |> fold (add_subterms []) ts end
   6.203  
   6.204  val term_max_depth = 2
   6.205 @@ -805,7 +802,7 @@
   6.206  
   6.207  fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
   6.208                             auto_level facts name_tabs th =
   6.209 -  case isar_dependencies_of name_tabs th of
   6.210 +  (case isar_dependencies_of name_tabs th of
   6.211      [] => (false, [])
   6.212    | isar_deps =>
   6.213      let
   6.214 @@ -819,9 +816,10 @@
   6.215        fun add_isar_dep facts dep accum =
   6.216          if exists (is_dep dep) accum then
   6.217            accum
   6.218 -        else case find_first (is_dep dep) facts of
   6.219 -          SOME ((_, status), th) => accum @ [(("", status), th)]
   6.220 -        | NONE => accum (* shouldn't happen *)
   6.221 +        else
   6.222 +          (case find_first (is_dep dep) facts of
   6.223 +            SOME ((_, status), th) => accum @ [(("", status), th)]
   6.224 +          | NONE => accum (* shouldn't happen *))
   6.225        val mepo_facts =
   6.226          facts
   6.227          |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
   6.228 @@ -838,7 +836,7 @@
   6.229          |> Output.urgent_message
   6.230        else
   6.231          ();
   6.232 -      case run_prover_for_mash ctxt params prover name facts goal of
   6.233 +      (case run_prover_for_mash ctxt params prover name facts goal of
   6.234          {outcome = NONE, used_facts, ...} =>
   6.235          (if verbose andalso auto_level = 0 then
   6.236             let val num_facts = length used_facts in
   6.237 @@ -849,8 +847,8 @@
   6.238           else
   6.239             ();
   6.240           (true, map fst used_facts))
   6.241 -      | _ => (false, isar_deps)
   6.242 -    end
   6.243 +      | _ => (false, isar_deps))
   6.244 +    end)
   6.245  
   6.246  
   6.247  (*** High-level communication with MaSh ***)
   6.248 @@ -1140,9 +1138,9 @@
   6.249                val access_G = access_G |> fold flop_wrt_access_graph flops
   6.250                val num_known_facts = num_known_facts + length learns
   6.251                val dirty =
   6.252 -                case (was_empty, dirty, relearns) of
   6.253 +                (case (was_empty, dirty, relearns) of
   6.254                    (false, SOME names, []) => SOME (map #1 learns @ names)
   6.255 -                | _ => NONE
   6.256 +                | _ => NONE)
   6.257              in
   6.258                MaSh.learn ctxt overlord (save andalso null relearns) (rev learns);
   6.259                MaSh.relearn ctxt overlord save relearns;
   6.260 @@ -1202,9 +1200,9 @@
   6.261              let
   6.262                val name = nickname_of_thm th
   6.263                val (n, relearns, flops) =
   6.264 -                case deps_of status th of
   6.265 +                (case deps_of status th of
   6.266                    SOME deps => (n + 1, (name, deps) :: relearns, flops)
   6.267 -                | NONE => (n, relearns, name :: flops)
   6.268 +                | NONE => (n, relearns, name :: flops))
   6.269                val (relearns, flops, next_commit) =
   6.270                  if Time.> (Timer.checkRealTimer timer, next_commit) then
   6.271                    (commit false [] relearns flops;
   6.272 @@ -1325,7 +1323,7 @@
   6.273            in
   6.274              if length facts - num_known_facts
   6.275                 <= max_facts_to_learn_before_query then
   6.276 -              case length (filter_out is_in_access_G facts) of
   6.277 +              (case length (filter_out is_in_access_G facts) of
   6.278                  0 => false
   6.279                | num_facts_to_learn =>
   6.280                  if num_facts_to_learn <= max_facts_to_learn_before_query then
   6.281 @@ -1333,21 +1331,21 @@
   6.282                     |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
   6.283                     true)
   6.284                  else
   6.285 -                  (maybe_launch_thread (); false)
   6.286 +                  (maybe_launch_thread (); false))
   6.287              else
   6.288                (maybe_launch_thread (); false)
   6.289            end
   6.290          else
   6.291            false
   6.292        val (save, effective_fact_filter) =
   6.293 -        case fact_filter of
   6.294 +        (case fact_filter of
   6.295            SOME ff => (ff <> mepoN andalso maybe_learn (), ff)
   6.296          | NONE =>
   6.297            if is_mash_enabled () then
   6.298              (maybe_learn (),
   6.299               if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
   6.300            else
   6.301 -            (false, mepoN)
   6.302 +            (false, mepoN))
   6.303  
   6.304        val unique_facts = drop_duplicate_facts facts
   6.305        val add_ths = Attrib.eval_thms ctxt add
   6.306 @@ -1373,11 +1371,11 @@
   6.307        val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take
   6.308      in
   6.309        if save then MaSh.save ctxt overlord else ();
   6.310 -      case (fact_filter, mess) of
   6.311 +      (case (fact_filter, mess) of
   6.312          (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
   6.313          [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
   6.314           (mashN, mash |> map fst |> add_and_take)]
   6.315 -      | _ => [(effective_fact_filter, mesh)]
   6.316 +      | _ => [(effective_fact_filter, mesh)])
   6.317      end
   6.318  
   6.319  fun kill_learners ctxt ({overlord, ...} : params) =
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Feb 03 15:19:07 2014 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Feb 03 15:33:18 2014 +0100
     7.3 @@ -171,7 +171,7 @@
     7.4          (not (is_irrelevant_const s) ? add_pconst_to_table (rich_pconst thy const x))
     7.5          #> fold (do_term false) ts
     7.6      and do_term ext_arg t =
     7.7 -      case strip_comb t of
     7.8 +      (case strip_comb t of
     7.9          (Const x, ts) => do_const true x ts
    7.10        | (Free x, ts) => do_const false x ts
    7.11        | (Abs (_, T, t'), ts) =>
    7.12 @@ -182,11 +182,11 @@
    7.13           ? add_pconst_to_table (pseudo_abs_name,
    7.14                                  PType (order_of_type T + 1, [])))
    7.15          #> fold (do_term false) (t' :: ts)
    7.16 -      | (_, ts) => fold (do_term false) ts
    7.17 +      | (_, ts) => fold (do_term false) ts)
    7.18      and do_term_or_formula ext_arg T =
    7.19        if T = HOLogic.boolT then do_formula else do_term ext_arg
    7.20      and do_formula t =
    7.21 -      case t of
    7.22 +      (case t of
    7.23          Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t'
    7.24        | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2
    7.25        | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
    7.26 @@ -212,7 +212,7 @@
    7.27          do_formula (t1 $ Bound ~1) #> do_formula t'
    7.28        | (t0 as Const (_, @{typ bool})) $ t1 =>
    7.29          do_term false t0 #> do_formula t1  (* theory constant *)
    7.30 -      | _ => do_term false t
    7.31 +      | _ => do_term false t)
    7.32    in do_formula end
    7.33  
    7.34  fun pconsts_in_fact thy t =
    7.35 @@ -233,17 +233,16 @@
    7.36    theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
    7.37  
    7.38  fun pair_consts_fact thy fudge fact =
    7.39 -  case fact |> snd |> theory_const_prop_of fudge
    7.40 -            |> pconsts_in_fact thy of
    7.41 +  (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of
    7.42      [] => NONE
    7.43 -  | consts => SOME ((fact, consts), NONE)
    7.44 +  | consts => SOME ((fact, consts), NONE))
    7.45  
    7.46  (* A two-dimensional symbol table counts frequencies of constants. It's keyed
    7.47     first by constant name and second by its list of type instantiations. For the
    7.48     latter, we need a linear ordering on "pattern list". *)
    7.49  
    7.50  fun patternT_ord p =
    7.51 -  case p of
    7.52 +  (case p of
    7.53      (Type (s, ps), Type (t, qs)) =>
    7.54      (case fast_string_ord (s, t) of
    7.55        EQUAL => dict_ord patternT_ord (ps, qs)
    7.56 @@ -253,7 +252,7 @@
    7.57    | (Type _, TVar _) => GREATER
    7.58    | (Type _, TFree _) => LESS
    7.59    | (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t)
    7.60 -  | (TFree _, _) => GREATER
    7.61 +  | (TFree _, _) => GREATER)
    7.62  fun ptype_ord (PType (m, ps), PType (n, qs)) =
    7.63    (case dict_ord patternT_ord (ps, qs) of
    7.64      EQUAL => int_ord (m, n)
    7.65 @@ -269,11 +268,11 @@
    7.66        |> Symtab.map_default (s, PType_Tab.empty)
    7.67        #> fold do_term ts
    7.68      and do_term t =
    7.69 -      case strip_comb t of
    7.70 +      (case strip_comb t of
    7.71          (Const x, ts) => do_const true x ts
    7.72        | (Free x, ts) => do_const false x ts
    7.73        | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
    7.74 -      | (_, ts) => fold do_term ts
    7.75 +      | (_, ts) => fold do_term ts)
    7.76    in do_term o theory_const_prop_of fudge o snd end
    7.77  
    7.78  fun pow_int _ 0 = 1.0
    7.79 @@ -356,7 +355,7 @@
    7.80  
    7.81  fun fact_weight fudge stature const_tab rel_const_tab chained_const_tab
    7.82                  fact_consts =
    7.83 -  case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab)
    7.84 +  (case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab)
    7.85                     ||> filter_out (pconst_hyper_mem swap rel_const_tab) of
    7.86      ([], _) => 0.0
    7.87    | (rel, irrel) =>
    7.88 @@ -373,7 +372,7 @@
    7.89                     o irrel_pconst_weight fudge const_tab chained_const_tab)
    7.90                    irrel
    7.91          val res = rel_weight / (rel_weight + irrel_weight)
    7.92 -      in if Real.isFinite res then res else 0.0 end
    7.93 +      in if Real.isFinite res then res else 0.0 end)
    7.94  
    7.95  fun take_most_relevant ctxt max_facts remaining_max
    7.96          ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
    7.97 @@ -411,15 +410,16 @@
    7.98    let
    7.99      fun aux _ _ NONE = NONE
   7.100        | aux t args (SOME tab) =
   7.101 -        case t of
   7.102 +        (case t of
   7.103            t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
   7.104          | Const (s, _) =>
   7.105            (if is_widely_irrelevant_const s then
   7.106               SOME tab
   7.107 -           else case Symtab.lookup tab s of
   7.108 -             NONE => SOME (Symtab.update (s, length args) tab)
   7.109 -           | SOME n => if n = length args then SOME tab else NONE)
   7.110 -        | _ => SOME tab
   7.111 +           else
   7.112 +             (case Symtab.lookup tab s of
   7.113 +               NONE => SOME (Symtab.update (s, length args) tab)
   7.114 +             | SOME n => if n = length args then SOME tab else NONE))
   7.115 +        | _ => SOME tab)
   7.116    in aux (prop_of th) [] end
   7.117  
   7.118  (* FIXME: This is currently only useful for polymorphic type encodings. *)
   7.119 @@ -507,11 +507,10 @@
   7.120                        :: hopeful) =
   7.121              let
   7.122                val weight =
   7.123 -                case cached_weight of
   7.124 +                (case cached_weight of
   7.125                    SOME w => w
   7.126                  | NONE =>
   7.127 -                  fact_weight fudge stature const_tab rel_const_tab
   7.128 -                              chained_const_tab fact_consts
   7.129 +                  fact_weight fudge stature const_tab rel_const_tab chained_const_tab fact_consts)
   7.130              in
   7.131                if weight >= thres then
   7.132                  relevant ((ax, weight) :: candidates) rejects hopeful
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 15:19:07 2014 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 15:33:18 2014 +0100
     8.3 @@ -215,10 +215,8 @@
     8.4      TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
     8.5    end
     8.6  
     8.7 -(* FIXME *)
     8.8 -fun timed_proof_method meth debug timeout ths =
     8.9 -  timed_apply timeout (silence_proof_methods debug
    8.10 -    #> (fn ctxt => tac_of_proof_method ctxt ([], ths) meth))
    8.11 +fun timed_proof_method meth timeout ths =
    8.12 +  timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
    8.13  
    8.14  fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
    8.15  
    8.16 @@ -248,9 +246,9 @@
    8.17                    ()
    8.18                val timer = Timer.startRealTimer ()
    8.19              in
    8.20 -              case timed_proof_method meth debug timeout ths state i of
    8.21 +              (case timed_proof_method meth timeout ths state i of
    8.22                  SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
    8.23 -              | _ => play timed_out meths
    8.24 +              | _ => play timed_out meths)
    8.25              end
    8.26              handle TimeLimit.TimeOut => play (meth :: timed_out) meths
    8.27        in
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Mon Feb 03 15:19:07 2014 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Mon Feb 03 15:33:18 2014 +0100
     9.3 @@ -38,7 +38,6 @@
     9.4    val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
     9.5    val string_of_play_outcome : play_outcome -> string
     9.6    val play_outcome_ord : play_outcome * play_outcome -> order
     9.7 -
     9.8    val one_line_proof_text : int -> one_line_params -> string
     9.9    val silence_proof_methods : bool -> Proof.context -> Proof.context
    9.10  end;