diff -r d4b69107a86a -r 203b4f5482c3 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Tue Jan 14 18:41:24 2014 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Wed Jan 15 08:01:36 2014 +0100
@@ -100,7 +100,7 @@
 subsubsection "Termination"
 
 locale Measure1 =
-fixes m :: "'av::{order,order_top} \<Rightarrow> nat"
+fixes m :: "'av::order_top \<Rightarrow> nat"
 fixes h :: "nat"
 assumes h: "m x \<le> h"
 begin