1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Nov 19 19:42:30 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Nov 19 22:20:01 2013 +0100
     1.3 @@ -29,19 +29,15 @@
     1.4    val forall_of : term -> term -> term
     1.5    val exists_of : term -> term -> term
     1.6    val unalias_type_enc : string -> string list
     1.7 -  val term_of_atp :
     1.8 -    Proof.context -> bool -> int Symtab.table -> typ option ->
     1.9 +  val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
    1.10      (string, string) atp_term -> term
    1.11 -  val prop_of_atp :
    1.12 -    Proof.context -> bool -> int Symtab.table ->
    1.13 +  val prop_of_atp : Proof.context -> bool -> int Symtab.table ->
    1.14      (string, string, (string, string) atp_term, string) atp_formula -> term
    1.15  
    1.16    val used_facts_in_atp_proof :
    1.17 -    Proof.context -> (string * stature) list vector -> string atp_proof ->
    1.18 -    (string * stature) list
    1.19 -  val used_facts_in_unsound_atp_proof :
    1.20 -    Proof.context -> (string * stature) list vector -> 'a atp_proof ->
    1.21 -    string list option
    1.22 +    Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list
    1.23 +  val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list vector ->
    1.24 +    'a atp_proof -> string list option
    1.25    val lam_trans_of_atp_proof : string atp_proof -> string -> string
    1.26    val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
    1.27    val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list ->

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 19 19:42:30 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 19 22:20:01 2013 +0100
     2.3 @@ -78,10 +78,7 @@
     2.4        (name, role, t, rule, []) :: lines
     2.5      else if role = Axiom then
     2.6        (* Facts are not proof lines. *)
     2.7 -      if is_only_type_information t then
     2.8 -        map (replace_dependencies_in_line (name, [])) lines
     2.9 -      else
    2.10 -        lines
    2.11 +      lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
    2.12      else
    2.13        map (replace_dependencies_in_line (name, [])) lines
    2.14    | add_line (line as (name, role, t, _, _)) lines =
    2.15 @@ -96,8 +93,7 @@
    2.16  
    2.17  (* Recursively delete empty lines (type information) from the proof. *)
    2.18  fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
    2.19 -    if is_only_type_information t then delete_dependency name lines
    2.20 -    else line :: lines
    2.21 +    if is_only_type_information t then delete_dependency name lines else line :: lines
    2.22    | add_nontrivial_line line lines = line :: lines
    2.23  and delete_dependency name lines =
    2.24    fold_rev add_nontrivial_line
    2.25 @@ -154,24 +150,17 @@
    2.26          let val l' = (prefix_of_depth depth prefix, next) in
    2.27            (l', (l, l') :: subst, next + 1)
    2.28          end
    2.29 -    fun do_facts subst =
    2.30 -      apfst (maps (the_list o AList.lookup (op =) subst))
    2.31 +    fun do_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
    2.32      fun do_assm depth (l, t) (subst, next) =
    2.33 -      let
    2.34 -        val (l, subst, next) =
    2.35 -          (l, subst, next) |> fresh_label depth assume_prefix
    2.36 -      in
    2.37 +      let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
    2.38          ((l, t), (subst, next))
    2.39        end
    2.40      fun do_assms subst depth (Assume assms) =
    2.41 -      fold_map (do_assm depth) assms (subst, 1)
    2.42 -      |> apfst Assume
    2.43 -      |> apsnd fst
    2.44 +      fold_map (do_assm depth) assms (subst, 1) |>> Assume ||> fst
    2.45      fun do_steps _ _ _ [] = []
    2.46        | do_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
    2.47          let
    2.48 -          val (l, subst, next) =
    2.49 -            (l, subst, next) |> fresh_label depth have_prefix
    2.50 +          val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
    2.51            val sub = do_proofs subst depth sub
    2.52            val by = by |> do_byline subst
    2.53          in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end
    2.54 @@ -224,9 +213,7 @@
    2.55      val (_, ctxt) =
    2.56        params
    2.57        |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
    2.58 -      |> (fn fixes =>
    2.59 -             ctxt |> Variable.set_body false
    2.60 -                  |> Proof_Context.add_fixes fixes)
    2.61 +      |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
    2.62      val one_line_proof = one_line_proof_text 0 one_line_params
    2.63      val do_preplay = preplay_timeout <> SOME Time.zeroTime
    2.64  
    2.65 @@ -265,8 +252,7 @@
    2.66          fun is_clause_skolemize_rule [(s, _)] =
    2.67              Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = SOME true
    2.68            | is_clause_skolemize_rule _ = false
    2.69 -        (* The assumptions and conjecture are "prop"s; the other formulas are
    2.70 -           "bool"s. *)
    2.71 +        (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s. *)
    2.72          fun prop_of_clause [(num, _)] =
    2.73              Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
    2.74            | prop_of_clause names =
    2.75 @@ -275,16 +261,14 @@
    2.76              in
    2.77                case List.partition (can HOLogic.dest_not) lits of
    2.78                  (negs as _ :: _, pos as _ :: _) =>
    2.79 -                s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
    2.80 -                       Library.foldr1 s_disj pos)
    2.81 +                s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
    2.82                | _ => fold (curry s_disj) lits @{term False}
    2.83              end
    2.84              |> HOLogic.mk_Trueprop |> close_form
    2.85          fun isar_proof_of_direct_proof infs =
    2.86            let
    2.87              fun maybe_show outer c =
    2.88 -              (outer andalso length c = 1 andalso subset (op =) (c, conjs))
    2.89 -              ? cons Show
    2.90 +              (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show
    2.91              val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
    2.92              fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
    2.93              fun do_steps outer predecessor accum [] =
    2.94 @@ -387,10 +371,8 @@
    2.95                 else
    2.96                   [])
    2.97            in
    2.98 -            "\n\nStructured proof"
    2.99 -              ^ (commas msg |> not (null msg) ? enclose " (" ")")
   2.100 -              ^ ":\n" ^
   2.101 -              Active.sendback_markup [Markup.padding_command] isar_text
   2.102 +            "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
   2.103 +            Active.sendback_markup [Markup.padding_command] isar_text
   2.104            end
   2.105        end
   2.106      val isar_proof =