# 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