changeset 26975 | 103dca19ef2e |
parent 25962 | 13b6c0b31005 |
child 27103 | d8549f4d900b |
--- a/src/HOL/Code_Setup.thy Fri May 23 16:37:57 2008 +0200 +++ b/src/HOL/Code_Setup.thy Fri May 23 16:41:39 2008 +0200 @@ -52,7 +52,7 @@ val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) in SOME (gr''', Codegen.parens - (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) + (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu])) end | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))