eq_codegen now ensures that code for bool type is generated.

--- a/src/HOL/HOL.thy	Sun Sep 25 20:17:44 2005 +0200
+++ b/src/HOL/HOL.thy	Sun Sep 25 20:19:31 2005 +0200
@@ -1211,9 +1211,10 @@
      | (Const ("op =", _), [t, u]) =>
           let
             val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
-            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
+            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
+            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
           in
-            SOME (gr'', Codegen.parens
+            SOME (gr''', Codegen.parens
               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
           end
      | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen