tuned: more standard use of order;

--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 17:27:13 2018 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 20:29:53 2018 +0100
@@ -895,7 +895,9 @@
         if h aconvc y then false else if h aconvc x then true else earlier t (x, y);
 
   fun earlier_ord vs (x, y) =
-    if x aconvc y then EQUAL else make_ord (earlier vs) (x, y);
+    if x aconvc y then EQUAL
+    else if earlier vs (x, y) then LESS
+    else GREATER;
 
 fun dest_frac ct =
   case Thm.term_of ct of

--- a/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 17:27:13 2018 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 20:29:53 2018 +0100
@@ -588,24 +588,26 @@
    (tm,(if is_semiring_constant tm then num_0 else num_1)));
 
 val morder =
- let fun lexorder l1 l2 =
-  case (l1,l2) of
+ let fun lexorder ls =
+  case ls of
     ([],[]) => 0
   | (_ ,[]) => ~1
   | ([], _) => 1
   | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
-     if is_less (variable_ord (x1, x2)) then 1
-     else if is_less (variable_ord (x2, x1)) then ~1
-     else if n1 < n2 then ~1
-     else if n2 < n1 then 1
-     else lexorder vs1 vs2
+     (case variable_ord (x1, x2) of
+       LESS => 1
+     | GREATER => ~1
+     | EQUAL =>
+         if n1 < n2 then ~1
+         else if n2 < n1 then 1
+         else lexorder (vs1, vs2))
  in fn tm1 => fn tm2 =>
   let val vdegs1 = map dest_varpow (powervars tm1)
       val vdegs2 = map dest_varpow (powervars tm2)
       val deg1 = fold (Integer.add o snd) vdegs1 num_0
       val deg2 = fold (Integer.add o snd) vdegs2 num_0
   in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
-                            else lexorder vdegs1 vdegs2
+                            else lexorder (vdegs1, vdegs2)
   end
  end;