tuned

--- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Apr 29 04:30:05 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Mon Apr 29 06:13:36 2013 +0200
@@ -130,7 +130,8 @@
 
 text{* Termination: *}
 
-definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"
+definition m_const :: "const \<Rightarrow> nat" where
+"m_const x = (if x = Any then 0 else 1)"
 
 interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const