--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 01 15:12:57 2018 +0100
@@ -420,7 +420,7 @@
(case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
(0, 1) =>
one_line_proof_text ctxt 0
- (if play_outcome_ord (play_outcome, one_line_play) = LESS then
+ (if is_less (play_outcome_ord (play_outcome, one_line_play)) then
(case isar_proof of
Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
let