# HG changeset patch
# User wenzelm
# Date 1517502118 -3600
# Node ID 6e5316a4307970a8cd7315e79f34e7f8552ebbea
# Parent  2427d3e72b6eeb5c2c1f79d51861baa72550554b
tuned;

diff -r 2427d3e72b6e -r 6e5316a43079 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 17:15:07 2018 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 17:21:58 2018 +0100
@@ -894,7 +894,8 @@
     | earlier (h::t) (x, y) =
         if h aconvc y then false else if h aconvc x then true else earlier t (x, y);
 
-  val earlier_ord = make_ord o earlier;
+  fun earlier_ord vs (x, y) =
+    if x aconvc y then EQUAL else make_ord (earlier vs) (x, y);
 
 fun dest_frac ct =
   case Thm.term_of ct of