diff -r 35807a5d8dc2 -r 2a1953f0d20d src/HOL/Codegenerator_Test/Generate_Pretty.thy --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy Sat Mar 24 16:27:04 2012 +0100 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Sun Mar 25 20:15:39 2012 +0200 @@ -10,9 +10,8 @@ lemma [code, code del]: "nat_of_char = nat_of_char" .. lemma [code, code del]: "char_of_nat = char_of_nat" .. -declare Quickcheck_Narrowing.zero_code_int_code[code del] -declare Quickcheck_Narrowing.one_code_int_code[code del] -declare Quickcheck_Narrowing.int_of_code[code del] +declare Quickcheck_Narrowing.one_code_int_code [code del] +declare Quickcheck_Narrowing.int_of_code [code del] subsection {* Check whether generated code compiles *}