1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Sun Dec 15 22:03:12 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Dec 16 08:35:03 2013 +0100
     1.3 @@ -13,28 +13,25 @@
     1.4  
     1.5    eqtype preplay_time
     1.6  
     1.7 -  datatype preplay_result =
     1.8 -    PplFail of exn |
     1.9 -    PplSucc of preplay_time
    1.10 +  type preplay_result
    1.11  
    1.12 -  val trace : bool Config.T
    1.13 -  val zero_preplay_time : preplay_time
    1.14 -  val some_preplay_time : preplay_time
    1.15 -  val add_preplay_time : preplay_time -> preplay_time -> preplay_time
    1.16 -  val string_of_preplay_time : preplay_time -> string
    1.17 +  val trace: bool Config.T
    1.18 +  val zero_preplay_time: preplay_time
    1.19 +  val some_preplay_time: preplay_time
    1.20 +  val add_preplay_time: preplay_time -> preplay_time -> preplay_time
    1.21 +  val string_of_preplay_time: preplay_time -> string
    1.22  
    1.23    type preplay_interface =
    1.24 -  { get_preplay_result : label -> preplay_result,
    1.25 -    set_preplay_result : label -> preplay_result -> unit,
    1.26 -    get_preplay_time : label -> preplay_time,
    1.27 -    set_preplay_time : label -> preplay_time -> unit,
    1.28 -    preplay_quietly : Time.time -> isar_step -> preplay_time,
    1.29 -    (* the returned flag signals a preplay failure *)
    1.30 -    overall_preplay_stats : isar_proof -> preplay_time * bool }
    1.31 +    {get_preplay_result: label -> preplay_result,
    1.32 +     set_preplay_result: label -> preplay_result -> unit,
    1.33 +     get_preplay_time: label -> preplay_time,
    1.34 +     set_preplay_time: label -> preplay_time -> unit,
    1.35 +     preplay_quietly: Time.time -> isar_step -> preplay_time,
    1.36 +     (* the returned flag signals a preplay failure *)
    1.37 +     overall_preplay_stats: isar_proof -> preplay_time * bool}
    1.38  
    1.39 -  val proof_preplay_interface :
    1.40 -    bool -> Proof.context -> string -> string -> bool -> Time.time
    1.41 -    -> isar_proof -> preplay_interface
    1.42 +  val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
    1.43 +    isar_proof -> preplay_interface
    1.44  end;
    1.45  
    1.46  structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
    1.47 @@ -53,8 +50,8 @@
    1.48  type preplay_time = bool * Time.time
    1.49  
    1.50  datatype preplay_result =
    1.51 -  PplFail of exn |
    1.52 -  PplSucc of preplay_time
    1.53 +  Preplay_Success of preplay_time |
    1.54 +  Preplay_Failure of exn
    1.55  
    1.56  val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
    1.57  val some_preplay_time = (true, Time.zeroTime)  (* > 0 ms *)
    1.58 @@ -63,199 +60,181 @@
    1.59  
    1.60  val string_of_preplay_time = ATP_Util.string_of_ext_time
    1.61  
    1.62 -(* preplay tracing *)
    1.63  fun preplay_trace ctxt assms concl time =
    1.64    let
    1.65      val ctxt = ctxt |> Config.put show_markup true
    1.66      val time = "[" ^ (string_of_preplay_time time) ^ "]" |> Pretty.str
    1.67      val nr_of_assms = length assms
    1.68 -    val assms = assms |> map (Display.pretty_thm ctxt)
    1.69 -                      |> (fn [] => Pretty.str ""
    1.70 -                           | [a] => a
    1.71 -                           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
    1.72 +    val assms = assms
    1.73 +      |> map (Display.pretty_thm ctxt)
    1.74 +      |> (fn [] => Pretty.str ""
    1.75 +           | [a] => a
    1.76 +           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
    1.77      val concl = concl |> Syntax.pretty_term ctxt
    1.78 -    val trace_list = [] |> cons concl
    1.79 -                        |> nr_of_assms>0 ? cons (Pretty.str "\<Longrightarrow>")
    1.80 -                        |> cons assms
    1.81 -                        |> cons time
    1.82 +    val trace_list = []
    1.83 +      |> cons concl
    1.84 +      |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>")
    1.85 +      |> cons assms
    1.86 +      |> cons time
    1.87      val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
    1.88 -  in tracing (Pretty.string_of pretty_trace) end
    1.89 +  in
    1.90 +    tracing (Pretty.string_of pretty_trace)
    1.91 +  end
    1.92  
    1.93 -(* timing *)
    1.94  fun take_time timeout tac arg =
    1.95 -  let
    1.96 -    val timing = Timing.start ()
    1.97 -  in
    1.98 +  let val timing = Timing.start () in
    1.99      (TimeLimit.timeLimit timeout tac arg;
   1.100 -      Timing.result timing |> #cpu |> pair false)
   1.101 +     Timing.result timing |> #cpu |> pair false)
   1.102      handle TimeLimit.TimeOut => (true, timeout)
   1.103    end
   1.104  
   1.105 -(* lookup facts in context *)
   1.106  fun resolve_fact_names ctxt names =
   1.107    (names
   1.108 -    |>> map string_of_label
   1.109 -    |> op @
   1.110 -    |> maps (thms_of_name ctxt))
   1.111 +   |>> map string_of_label
   1.112 +   |> op @
   1.113 +   |> maps (thms_of_name ctxt))
   1.114    handle ERROR msg => error ("preplay error: " ^ msg)
   1.115  
   1.116 -(* turn terms/proofs into theorems *)
   1.117 -fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
   1.118 -
   1.119  fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
   1.120    let
   1.121 +    val thy = Proof_Context.theory_of ctxt
   1.122 +
   1.123      val concl = 
   1.124        (case try List.last steps of
   1.125          SOME (Prove (_, [], _, t, _, _)) => t
   1.126        | _ => raise Fail "preplay error: malformed subproof")
   1.127 +
   1.128      val var_idx = maxidx_of_term concl + 1
   1.129 -    fun var_of_free (x, T) = Var((x, var_idx), T)
   1.130 -    val substitutions =
   1.131 -      map (`var_of_free #> swap #> apfst Free) fixed_frees
   1.132 +    fun var_of_free (x, T) = Var ((x, var_idx), T)
   1.133 +    val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees
   1.134    in
   1.135      Logic.list_implies (assms |> map snd, concl)
   1.136 -      |> subst_free substitutions
   1.137 -      |> thm_of_term ctxt
   1.138 +    |> subst_free subst
   1.139 +    |> Skip_Proof.make_thm thy
   1.140    end
   1.141  
   1.142 -(* mapping from proof methods to tactics *)
   1.143  fun tac_of_method method type_enc lam_trans ctxt facts =
   1.144 -  case method of
   1.145 +  (case method of
   1.146      MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
   1.147    | _ =>
   1.148 -      Method.insert_tac facts
   1.149 -      THEN' (case method of
   1.150 -              SimpM => Simplifier.asm_full_simp_tac
   1.151 -            | AutoM => Clasimp.auto_tac #> K
   1.152 -            | FastforceM => Clasimp.fast_force_tac
   1.153 -            | ForceM => Clasimp.force_tac
   1.154 -            | ArithM => Arith_Data.arith_tac
   1.155 -            | BlastM => blast_tac
   1.156 -            | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
   1.157 +      Method.insert_tac facts THEN'
   1.158 +      (case method of
   1.159 +        SimpM => Simplifier.asm_full_simp_tac
   1.160 +      | AutoM => Clasimp.auto_tac #> K
   1.161 +      | FastforceM => Clasimp.fast_force_tac
   1.162 +      | ForceM => Clasimp.force_tac
   1.163 +      | ArithM => Arith_Data.arith_tac
   1.164 +      | BlastM => blast_tac
   1.165 +      | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt)
   1.166  
   1.167 -
   1.168 -(* main function for preplaying isar_steps; may throw exceptions *)
   1.169 +(* main function for preplaying Isar steps; may throw exceptions *)
   1.170  fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
   1.171    | preplay_raw debug type_enc lam_trans ctxt timeout
   1.172 -      (Prove (_, xs, _, t, subproofs, (fact_names, proof_method))) =
   1.173 -  let
   1.174 -    val (prop, obtain) =
   1.175 -      (case xs of
   1.176 -        [] => (t, false)
   1.177 -      | _ =>
   1.178 -      (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
   1.179 -           (see ~~/src/Pure/Isar/obtain.ML) *)
   1.180 -        let
   1.181 -          val thesis = Term.Free ("thesis", HOLogic.boolT)
   1.182 -          val thesis_prop = thesis |> HOLogic.mk_Trueprop
   1.183 -          val frees = map Term.Free xs
   1.184 +      (step as Prove (_, xs, _, t, subproofs, (fact_names, meth))) =
   1.185 +    let
   1.186 +      val prop =
   1.187 +        (case xs of
   1.188 +          [] => t
   1.189 +        | _ =>
   1.190 +          (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
   1.191 +             (cf. "~~/src/Pure/Isar/obtain.ML") *)
   1.192 +          let
   1.193 +            val thesis = Term.Free ("thesis", HOLogic.boolT)
   1.194 +            val thesis_prop = thesis |> HOLogic.mk_Trueprop
   1.195 +            val frees = map Term.Free xs
   1.196  
   1.197 -          (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
   1.198 -          val inner_prop =
   1.199 -            fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
   1.200 +            (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
   1.201 +            val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
   1.202 +          in
   1.203 +            (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
   1.204 +            Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
   1.205 +          end)
   1.206  
   1.207 -          (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
   1.208 -          val prop =
   1.209 -            Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
   1.210 -        in
   1.211 -          (prop, true)
   1.212 -        end)
   1.213 -    val facts =
   1.214 -      map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
   1.215 -    val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
   1.216 -                    |> Config.put Lin_Arith.verbose debug
   1.217 -                    |> obtain ? Config.put Metis_Tactic.new_skolem true
   1.218 -    val goal =
   1.219 -      Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop
   1.220 -    fun tac {context = ctxt, prems = _} =
   1.221 -      HEADGOAL (tac_of_method proof_method type_enc lam_trans ctxt facts)
   1.222 -    fun run_tac () = goal tac
   1.223 -      handle ERROR msg => error ("Preplay error: " ^ msg)
   1.224 -    val preplay_time = take_time timeout run_tac ()
   1.225 -  in
   1.226 -    (* tracing *)
   1.227 -    (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time
   1.228 -     else ();
   1.229 -     preplay_time)
   1.230 -  end
   1.231 +      val facts = map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
   1.232 +
   1.233 +      val ctxt = ctxt
   1.234 +        |> Config.put Metis_Tactic.verbose debug
   1.235 +        |> Config.put Lin_Arith.verbose debug
   1.236 +        |> use_metis_new_skolem step ? Config.put Metis_Tactic.new_skolem true
   1.237 +
   1.238 +      val goal = Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop
   1.239 +
   1.240 +      fun tac {context = ctxt, ...} = HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts)
   1.241 +      fun run_tac () = goal tac handle ERROR msg => error ("Preplay error: " ^ msg)
   1.242 +
   1.243 +      val preplay_time = take_time timeout run_tac ()
   1.244 +    in
   1.245 +      (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time else ();
   1.246 +       preplay_time)
   1.247 +    end
   1.248  
   1.249  
   1.250  (*** proof preplay interface ***)
   1.251  
   1.252  type preplay_interface =
   1.253 -{ get_preplay_result : label -> preplay_result,
   1.254 -  set_preplay_result : label -> preplay_result -> unit,
   1.255 -  get_preplay_time : label -> preplay_time,
   1.256 -  set_preplay_time : label -> preplay_time -> unit,
   1.257 -  preplay_quietly : Time.time -> isar_step -> preplay_time,
   1.258 -  (* the returned flag signals a preplay failure *)
   1.259 -  overall_preplay_stats : isar_proof -> preplay_time * bool }
   1.260 +  {get_preplay_result: label -> preplay_result,
   1.261 +   set_preplay_result: label -> preplay_result -> unit,
   1.262 +   get_preplay_time: label -> preplay_time,
   1.263 +   set_preplay_time: label -> preplay_time -> unit,
   1.264 +   preplay_quietly: Time.time -> isar_step -> preplay_time,
   1.265 +   (* the returned flag signals a preplay failure *)
   1.266 +   overall_preplay_stats: isar_proof -> preplay_time * bool}
   1.267  
   1.268 -
   1.269 -(* enriches context with local proof facts *)
   1.270 -fun enrich_context proof ctxt =
   1.271 +fun enrich_context_with_local_facts proof ctxt =
   1.272    let
   1.273      val thy = Proof_Context.theory_of ctxt
   1.274  
   1.275      fun enrich_with_fact l t =
   1.276 -      Proof_Context.put_thms false
   1.277 -        (string_of_label l, SOME [Skip_Proof.make_thm thy t])
   1.278 +      Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
   1.279  
   1.280      val enrich_with_assms = fold (uncurry enrich_with_fact)
   1.281  
   1.282      fun enrich_with_proof (Proof (_, assms, isar_steps)) =
   1.283        enrich_with_assms assms #> fold enrich_with_step isar_steps
   1.284 -
   1.285      and enrich_with_step (Let _) = I
   1.286        | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
   1.287 -          enrich_with_fact l t #> fold enrich_with_proof subproofs
   1.288 +        enrich_with_fact l t #> fold enrich_with_proof subproofs
   1.289    in
   1.290      enrich_with_proof proof ctxt
   1.291    end
   1.292  
   1.293 -
   1.294 -(* Given a proof, produces an imperative preplay interface with a shared table
   1.295 -   mapping from labels to preplay results.
   1.296 -   The preplay results are caluclated lazyly and cached to avoid repeated
   1.297 +(* Given a proof, produces an imperative preplay interface with a shared table mapping from labels
   1.298 +   to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated
   1.299     calculation.
   1.300  
   1.301 -   PRECONDITION: the proof must be labeled canocially, see
   1.302 -   Slegehammer_Proof.relabel_proof_canonically
   1.303 -*)
   1.304 -
   1.305 -fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
   1.306 -      preplay_timeout proof : preplay_interface =
   1.307 +   Precondition: The proof must be labeled canocially; cf.
   1.308 +   "Slegehammer_Proof.relabel_proof_canonically". *)
   1.309 +fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
   1.310    if not do_preplay then
   1.311      (* the dont_preplay option pretends that everything works just fine *)
   1.312 -    { get_preplay_result = K (PplSucc zero_preplay_time),
   1.313 -      set_preplay_result = K (K ()),
   1.314 -      get_preplay_time = K zero_preplay_time,
   1.315 -      set_preplay_time = K (K ()),
   1.316 -      preplay_quietly = K (K zero_preplay_time),
   1.317 -      overall_preplay_stats = K (zero_preplay_time, false)}
   1.318 +    {get_preplay_result = K (Preplay_Success zero_preplay_time),
   1.319 +     set_preplay_result = K (K ()),
   1.320 +     get_preplay_time = K zero_preplay_time,
   1.321 +     set_preplay_time = K (K ()),
   1.322 +     preplay_quietly = K (K zero_preplay_time),
   1.323 +     overall_preplay_stats = K (zero_preplay_time, false)} : preplay_interface
   1.324    else
   1.325      let
   1.326 -      (* add local proof facts to context *)
   1.327 -      val ctxt = enrich_context proof ctxt
   1.328 +      val ctxt = enrich_context_with_local_facts proof ctxt
   1.329  
   1.330        fun preplay quietly timeout step =
   1.331          preplay_raw debug type_enc lam_trans ctxt timeout step
   1.332 -        |> PplSucc
   1.333 +        |> Preplay_Success
   1.334          handle exn =>
   1.335 -          if Exn.is_interrupt exn then
   1.336 -            reraise exn
   1.337 -          else if not quietly andalso debug then
   1.338 -            (warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  "
   1.339 -                      ^ @{make_string} exn);
   1.340 -             PplFail exn)
   1.341 -          else
   1.342 -            PplFail exn
   1.343 +               if Exn.is_interrupt exn then
   1.344 +                 reraise exn
   1.345 +               else if not quietly andalso debug then
   1.346 +                 (warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  " ^
   1.347 +                    @{make_string} exn);
   1.348 +                  Preplay_Failure exn)
   1.349 +               else
   1.350 +                 Preplay_Failure exn
   1.351  
   1.352        (* preplay steps treating exceptions like timeouts *)
   1.353        fun preplay_quietly timeout step =
   1.354          (case preplay true timeout step of
   1.355 -          PplSucc preplay_time => preplay_time
   1.356 -        | PplFail _ => (true, timeout))
   1.357 +          Preplay_Success preplay_time => preplay_time
   1.358 +        | Preplay_Failure _ => (true, timeout))
   1.359  
   1.360        val preplay_tab =
   1.361          let
   1.362 @@ -263,46 +242,41 @@
   1.363              case label_of_step step of
   1.364                NONE => tab
   1.365              | SOME l =>
   1.366 -                Canonical_Lbl_Tab.update_new
   1.367 -                  (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy)
   1.368 -                  tab
   1.369 -            handle Canonical_Lbl_Tab.DUP _ =>
   1.370 -              raise Fail "Sledgehammer_Preplay: preplay time table"
   1.371 +              Canonical_Lbl_Tab.update_new
   1.372 +                (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab
   1.373 +            handle Canonical_Lbl_Tab.DUP _ => raise Fail "Sledgehammer_Preplay: preplay time table"
   1.374          in
   1.375            Canonical_Lbl_Tab.empty
   1.376            |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
   1.377            |> Unsynchronized.ref
   1.378          end
   1.379  
   1.380 -      fun get_preplay_result lbl =
   1.381 -        Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
   1.382 -        handle Option.Option =>
   1.383 -          raise Fail "Sledgehammer_Preplay: preplay time table"
   1.384 +      fun get_preplay_result l =
   1.385 +        Canonical_Lbl_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
   1.386 +        handle Option.Option => raise Fail "Sledgehammer_Preplay: preplay time table"
   1.387  
   1.388 -      fun set_preplay_result lbl result =
   1.389 -        preplay_tab :=
   1.390 -          Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab)
   1.391 +      fun set_preplay_result l result =
   1.392 +        preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
   1.393  
   1.394 -      fun get_preplay_time lbl =
   1.395 -        case get_preplay_result lbl of
   1.396 -          PplSucc preplay_time => preplay_time
   1.397 -        | PplFail _ => some_preplay_time (* best approximation possible *)
   1.398 +      fun get_preplay_time l =
   1.399 +        (case get_preplay_result l of
   1.400 +          Preplay_Success preplay_time => preplay_time
   1.401 +        | Preplay_Failure _ => some_preplay_time)
   1.402  
   1.403 -      fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time)
   1.404 +      fun set_preplay_time l time = set_preplay_result l (Preplay_Success time)
   1.405  
   1.406 -      fun overall_preplay_stats (Proof(_, _, steps)) =
   1.407 +      fun overall_preplay_stats (Proof (_, _, steps)) =
   1.408          let
   1.409            fun result_of_step step =
   1.410              try (label_of_step #> the #> get_preplay_result) step
   1.411 -            |> the_default (PplSucc zero_preplay_time)
   1.412 +            |> the_default (Preplay_Success zero_preplay_time)
   1.413            fun do_step step =
   1.414              (case result_of_step step of
   1.415 -              PplSucc preplay_time => apfst (add_preplay_time preplay_time)
   1.416 -            | PplFail _ => apsnd (K true))
   1.417 +              Preplay_Success preplay_time => apfst (add_preplay_time preplay_time)
   1.418 +            | Preplay_Failure _ => apsnd (K true))
   1.419          in
   1.420            fold_isar_steps do_step steps (zero_preplay_time, false)
   1.421          end
   1.422 -
   1.423      in
   1.424        {get_preplay_result = get_preplay_result,
   1.425         set_preplay_result = set_preplay_result,

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Sun Dec 15 22:03:12 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Mon Dec 16 08:35:03 2013 +0100
     2.3 @@ -172,8 +172,8 @@
     2.4              |> maybe_quote),
     2.5         ctxt |> Variable.auto_fixes term)
     2.6  
     2.7 -    fun by_method method = "by " ^
     2.8 -      (case method of
     2.9 +    fun by_method meth = "by " ^
    2.10 +      (case meth of
    2.11          SimpM => "simp"
    2.12        | AutoM => "auto"
    2.13        | FastforceM => "fastforce"
    2.14 @@ -187,16 +187,15 @@
    2.15            "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
    2.16  
    2.17      fun of_method ls ss MetisM =
    2.18 -          reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
    2.19 -      | of_method ls ss method =
    2.20 -          using_facts ls ss ^ by_method method
    2.21 +        reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
    2.22 +      | of_method ls ss meth = using_facts ls ss ^ by_method meth
    2.23  
    2.24 -    fun of_byline ind options (ls, ss) method =
    2.25 +    fun of_byline ind options (ls, ss) meth =
    2.26        let
    2.27          val ls = ls |> sort_distinct label_ord
    2.28          val ss = ss |> sort_distinct string_ord
    2.29        in
    2.30 -        "\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss method
    2.31 +        "\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss meth
    2.32        end
    2.33  
    2.34      fun of_free (s, T) =
    2.35 @@ -219,10 +218,10 @@
    2.36  
    2.37      fun add_assms ind assms = fold (add_assm ind) assms
    2.38  
    2.39 -    fun add_step_post ind l t facts method options =
    2.40 +    fun add_step_post ind l t facts meth options =
    2.41        add_suffix (of_label l)
    2.42        #> add_term t
    2.43 -      #> add_suffix (of_byline ind options facts method ^ "\n")
    2.44 +      #> add_suffix (of_byline ind options facts meth ^ "\n")
    2.45  
    2.46      fun of_subproof ind ctxt proof =
    2.47        let
    2.48 @@ -251,23 +250,21 @@
    2.49          #> add_suffix " = "
    2.50          #> add_term t2
    2.51          #> add_suffix "\n"
    2.52 -      | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, method))) =
    2.53 +      | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, meth))) =
    2.54          (case xs of
    2.55            [] => (* have *)
    2.56              add_step_pre ind qs subproofs
    2.57              #> add_suffix (of_prove qs (length subproofs) ^ " ")
    2.58 -            #> add_step_post ind l t facts method ""
    2.59 +            #> add_step_post ind l t facts meth ""
    2.60          | _ => (* obtain *)
    2.61              add_step_pre ind qs subproofs
    2.62              #> add_suffix (of_obtain qs (length subproofs) ^ " ")
    2.63              #> add_frees xs
    2.64              #> add_suffix " where "
    2.65 -            (* The new skolemizer puts the arguments in the same order as the
    2.66 -               ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML"
    2.67 -               regarding Vampire). *)
    2.68 -            #> add_step_post ind l t facts method
    2.69 -                 (if exists (fn (_, T) => length (binder_types T) > 1) xs
    2.70 -                  andalso method = MetisM then
    2.71 +            (* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire --
    2.72 +               but see also "atp_proof_reconstruct.ML" regarding Vampire). *)
    2.73 +            #> add_step_post ind l t facts meth
    2.74 +                 (if use_metis_new_skolem step then
    2.75                      "using [[metis_new_skolem]] "
    2.76                    else
    2.77                      ""))

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Sun Dec 15 22:03:12 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Dec 16 08:35:03 2013 +0100
     3.3 @@ -45,6 +45,7 @@
     3.4    val subproofs_of_step : isar_step -> isar_proof list option
     3.5    val byline_of_step : isar_step -> (facts * proof_method) option
     3.6    val proof_method_of_step : isar_step -> proof_method option
     3.7 +  val use_metis_new_skolem : isar_step -> bool
     3.8  
     3.9    val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
    3.10    val fold_isar_steps :
    3.11 @@ -59,7 +60,6 @@
    3.12    val relabel_proof_canonically : isar_proof -> isar_proof
    3.13  
    3.14    structure Canonical_Lbl_Tab : TABLE
    3.15 -
    3.16  end;
    3.17  
    3.18  structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
    3.19 @@ -110,6 +110,10 @@
    3.20  fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method
    3.21    | proof_method_of_step _ = NONE
    3.22  
    3.23 +fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth))) =
    3.24 +    meth = MetisM andalso exists (fn (_, T) => length (binder_types T) > 1) xs
    3.25 +  | use_metis_new_skolem _ = false
    3.26 +
    3.27  fun fold_isar_steps f = fold (fold_isar_step f)
    3.28  and fold_isar_step f step s =
    3.29    fold (steps_of_proof #> fold_isar_steps f)