src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

       lines (* axioms (facts) need no proof lines *)
     else
       map (replace_dependencies_in_line (name, [])) lines
   | add_line_pass1 line lines = line :: lines
 
-fun normalize role t =
-  t |> role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
+fun normalize role =
+  role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
 
 fun add_lines_pass2 res [] = rev res
   | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
     let
       val norm_t = normalize role t

 
         fun isar_steps outer predecessor accum [] =
             accum
             |> (if tainted = [] then
                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
-                    (the_list predecessor, []), massage_methods systematic_methods', ""))
+                    sort_facts (the_list predecessor, []), massage_methods systematic_methods', ""))
                 else
                   I)
             |> rev
           | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
             let
               val l = label_of_clause c
               val t = prop_of_clause c
               val rule = rule_of_clause_id id
               val skolem = is_skolemize_rule rule
 
-              val deps = fold add_fact_of_dependencies gamma ([], [])
+              val deps = ([], [])
+                |> fold add_fact_of_dependencies gamma
+                |> sort_facts
               val meths =
                 (if skolem then skolem_methods
                  else if is_arith_rule rule then arith_methods
                  else if is_datatype_rule rule then datatype_methods
                  else systematic_methods')

               val l = label_of_clause c
               val t = prop_of_clause c
               val step =
                 Prove (maybe_show outer c [], [], l, t,
                   map isar_case (filter_out (null o snd) cases),
-                  (the_list predecessor, []), massage_methods systematic_methods', "")
+                  sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")
             in
               isar_steps outer (SOME l) (step :: accum) infs
             end
         and isar_proof outer fix assms lems infs =
           Proof (fix, assms, lems @ isar_steps outer NONE [] infs)