# HG changeset patch
# User nipkow
# Date 1389769296 -3600
# Node ID 203b4f5482c32e9c43976e34860c88b281f2c64e
# Parent  d4b69107a86ae1964529efb2b70ae01e7c052ce2
tuned

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