--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Aug 04 13:06:24 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Aug 04 13:13:10 2014 +0200
@@ -41,7 +41,8 @@
let
val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
- fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
+ fun mk_step_lfs_gfs lfs gfs =
+ Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment)
fun minimize_half _ min_facts [] time = (min_facts, time)
| minimize_half mk_step min_facts (fact :: facts) time =