diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/Classpackage.thy --- a/src/HOL/ex/Classpackage.thy Thu Aug 31 23:01:16 2006 +0200 +++ b/src/HOL/ex/Classpackage.thy Fri Sep 01 08:36:51 2006 +0200 @@ -319,10 +319,10 @@ "x2 = X (1::int) 2 3" "y2 = Y (1::int) 2 3" -code_generate "op \" \ inv -code_generate (ml, haskell) X Y -code_generate (ml, haskell) x1 x2 y2 +code_gen "op \" \ inv +code_gen X Y (SML) (Haskell) +code_gen x1 x2 y2 (SML) (Haskell) -code_serialize ml (-) +code_gen (SML -) end