src/HOL/IMP/Abs_Int3.thy
changeset 49399 a9d9f3483b71
parent 49396 73fb17ed2e08
child 49496 2694d1615eef
--- a/src/HOL/IMP/Abs_Int3.thy	Sun Sep 16 20:16:28 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Mon Sep 17 02:25:38 2012 +0200
@@ -383,7 +383,7 @@
 
 subsubsection "Tests"
 
-(* FIXME dirty trick to get around some problem with the code generator *)
+(* Trick to make the code generator happy. *)
 lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y"
 by(rule refl)