src/HOL/ex/Classpackage.thy
changeset 22074 de3586cb0ebd
parent 21924 fe474e69e603
child 22179 1a3575de2afc
     1.1 --- a/src/HOL/ex/Classpackage.thy	Tue Jan 16 13:59:08 2007 +0100
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Jan 16 14:10:24 2007 +0100
     1.3 @@ -327,8 +327,7 @@
     1.4  definition "x2 = X (1::int) 2 3"
     1.5  definition "y2 = Y (1::int) 2 3"
     1.6  
     1.7 -code_gen "op \<otimes>" \<one> inv
     1.8 -code_gen X Y (SML #) (Haskell -) (OCaml -)
     1.9 -code_gen x1 x2 y2 (SML #) (Haskell -) (OCaml -)
    1.10 +code_gen "op \<otimes>" \<one> inv X Y
    1.11 +code_gen x1 x2 y2 (SML #) (OCaml -) (Haskell -)
    1.12  
    1.13  end