--- a/src/HOL/IMP/Abs_Int1_parity.thy Wed Sep 12 23:38:12 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Thu Sep 13 10:28:48 2012 +0200
@@ -108,7 +108,7 @@
text{* Instantiating the abstract interpretation locale requires no more
proofs (they happened in the instatiation above) but delivers the
-instantiated abstract interpreter which we call AI: *}
+instantiated abstract interpreter which we call @{text AI_parity}: *}
interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity