
diff -r 6535c537b243 -r 3c7610b8dcfc src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Wed Feb 19 22:05:05 2014 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Wed Feb 19 22:05:15 2014 +0100
@@ -69,7 +69,7 @@
 
 permanent_interpretation Abs_Int
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defines AI_const is AI and step_const is step' and aval'_const is aval'
+defining AI_const = AI and step_const = step' and aval'_const = aval'
 ..
 
 




