tuning
authorblanchet
Fri Jan 31 18:43:16 2014 +0100 (2014-01-31)
changeset 5521770035950e19b
parent 55216 77953325d5f1
child 55218 ed495a5088c6
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     1.3 @@ -235,12 +235,6 @@
     1.4  
     1.5      fun add_assms ind assms = fold (add_assm ind) assms
     1.6  
     1.7 -    fun add_step_post ind l t (ls, ss) meth =
     1.8 -      add_str (of_label l)
     1.9 -      #> add_term t
    1.10 -      #> add_str (" " ^
    1.11 -           of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ "\n")
    1.12 -
    1.13      fun of_subproof ind ctxt proof =
    1.14        let
    1.15          val ind = ind + 1
    1.16 @@ -262,13 +256,16 @@
    1.17          add_str (of_indent ind ^ "let ")
    1.18          #> add_term t1 #> add_str " = " #> add_term t2
    1.19          #> add_str "\n"
    1.20 -      | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
    1.21 +      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), (meth :: _) :: _))) =
    1.22          add_step_pre ind qs subproofs
    1.23          #> (case xs of
    1.24               [] => add_str (of_have qs (length subproofs) ^ " ")
    1.25             | _ =>
    1.26               add_str (of_obtain qs (length subproofs) ^ " ") #> add_frees xs #> add_str " where ")
    1.27 -        #> add_step_post ind l t facts meth
    1.28 +        #> add_str (of_label l)
    1.29 +        #> add_term t
    1.30 +        #> add_str (" " ^
    1.31 +             of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ "\n")
    1.32      and add_steps ind = fold (add_step ind)
    1.33      and of_proof ind ctxt (Proof (xs, assms, steps)) =
    1.34        ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst