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