1.1 --- a/src/HOL/HOL.thy Tue Apr 22 13:35:26 2008 +0200
1.2 +++ b/src/HOL/HOL.thy Tue Apr 22 22:00:25 2008 +0200
1.3 @@ -1659,8 +1659,6 @@
1.4
1.5 subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *}
1.6
1.7 -setup "CodeName.setup #> CodeTarget.setup #> Nbe.setup"
1.8 -
1.9 code_datatype Trueprop "prop"
1.10
1.11 code_datatype "TYPE('a\<Colon>{})"
1.12 @@ -1699,6 +1697,9 @@
1.13
1.14 setup {*
1.15 CodeUnit.add_const_alias @{thm equals_eq}
1.16 + #> CodeName.setup
1.17 + #> CodeTarget.setup
1.18 + #> Nbe.setup @{sort eq} [(@{const_name eq_class.eq}, @{const_name "op ="})]
1.19 *}
1.20
1.21 lemma [code func]: