diff -r 3f3223b90239 -r e051eea34990 src/HOL/Data_Structures/Cmp.thy
--- a/src/HOL/Data_Structures/Cmp.thy	Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Data_Structures/Cmp.thy	Thu Jul 07 18:08:02 2016 +0200
@@ -1,4 +1,4 @@
-(* Author: Tobias Nipkow *)
+(* Author: Tobias Nipkow, Daniel Stüwe *)
 
 section {* Three-Way Comparison *}
 
@@ -6,16 +6,23 @@
 imports Main
 begin
 
-datatype cmp = LT | EQ | GT
+datatype cmp_val = LT | EQ | GT
 
-class cmp = linorder +
-fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> cmp"
-assumes LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
-assumes EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
-assumes GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
+function cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where
+"x < y \<Longrightarrow> cmp x y = LT" |
+"x = y \<Longrightarrow> cmp x y = EQ" |
+"x > y \<Longrightarrow> cmp x y = GT"
+by (auto, force)
+termination by lexicographic_order
+
+lemma 
+    LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
+and EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
+and GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
+by (cases x y rule: linorder_cases, auto)+
 
 lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) =
   (if c = LT then l else if c = GT then g else e)"
-by(simp split: cmp.split)
+by(simp split: cmp_val.split)
 
 end