Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
changeset 57776 1111a9a328fe
parent 57750 670cbec816b9
child 57781 c1ce4ef23be5 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Aug 04 12:28:42 2014 +0200
@@ -73,7 +73,7 @@
 fun n_facts names =
   let val n = length names in
     string_of_int n ^ " fact" ^ plural_s n ^
-    (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
+    (if n > 0 then ": " ^ (names |> map fst |> space_implode " ") else "")
   end
 
 fun print silent f = if silent then () else Output.urgent_message (f ())
isabelle