# HG changeset patch
# User nipkow
# Date 1367208816 -7200
# Node ID 71260347b7e4c123dd6e3e928b287288be8217f4
# Parent  496c0ef8990cda1ab98b9c78f13e9481a383fced
tuned

diff -r 496c0ef8990c -r 71260347b7e4 src/HOL/IMP/Abs_Int1_const.thy
--- 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