# HG changeset patch
# User berghofe
# Date 1127672371 -7200
# Node ID 50878db27b9497e030e2d286bc5a33b1a4aadc45
# Parent  6de497c99e4c9aae761737310a4d1b5b054981fa
eq_codegen now ensures that code for bool type is generated.

diff -r 6de497c99e4c -r 50878db27b94 src/HOL/HOL.thy
--- 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