changeset 57776 | 1111a9a328fe |
parent 57774 | d2ad1320c770 |
child 57777 | 563df8185d98 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 04 11:54:23 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 04 12:28:42 2014 +0200 @@ -78,7 +78,7 @@ dont_know () else let - val fact_names = used_facts |> map fst |> sort string_ord + val fact_names = map fst used_facts val {context = ctxt, facts = chained, goal} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt