src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 46342 c59b8560eb48
parent 46340 cac402c486b0
child 46365 547d1a1dcaf6
equal deleted inserted replaced
46341:ab9d96cc7a99 46342:c59b8560eb48
   246     case minimize_command ss of
   246     case minimize_command ss of
   247       "" => ""
   247       "" => ""
   248     | command =>
   248     | command =>
   249       "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
   249       "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
   250 
   250 
   251 val split_used_facts =
   251 fun split_used_facts facts =
   252   List.partition (fn (_, (sc, _)) => sc = Chained)
   252   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
   253   #> pairself (sort_distinct (string_ord o pairself fst))
   253         |> pairself (sort_distinct (string_ord o pairself fst))
   254 
   254 
   255 fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
   255 fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
   256                          subgoal, subgoal_count) =
   256                          subgoal, subgoal_count) =
   257   let
   257   let
   258     val (chained, extra) = split_used_facts used_facts
   258     val (chained, extra) = split_used_facts used_facts