src/HOL/Code_Setup.thy
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))