cleanup

--- a/src/HOL/ex/Classpackage.thy	Tue Jan 16 13:59:08 2007 +0100
+++ b/src/HOL/ex/Classpackage.thy	Tue Jan 16 14:10:24 2007 +0100
@@ -327,8 +327,7 @@
 definition "x2 = X (1::int) 2 3"
 definition "y2 = Y (1::int) 2 3"
 
-code_gen "op \<otimes>" \<one> inv
-code_gen X Y (SML #) (Haskell -) (OCaml -)
-code_gen x1 x2 y2 (SML #) (Haskell -) (OCaml -)
+code_gen "op \<otimes>" \<one> inv X Y
+code_gen x1 x2 y2 (SML #) (OCaml -) (Haskell -)
 
 end

--- a/src/Pure/Tools/class_package.ML	Tue Jan 16 13:59:08 2007 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Jan 16 14:10:24 2007 +0100
@@ -388,6 +388,8 @@
     |> do_proof after_qed (loc_name, loc_expr)
   end;
 
+val prove_instance_sort = instance_sort' o prove_interpretation_in;
+
 
 (* classes and instances *)
 
@@ -487,8 +489,6 @@
 
 local
 
-val prove_instance_sort = instance_sort' o prove_interpretation_in;
-
 fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
   let
     val class = prep_class theory raw_class;
@@ -507,7 +507,6 @@
 
 val instance_sort_e = gen_instance_sort Sign.read_class Sign.read_sort;
 val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;
-val prove_instance_sort = prove_instance_sort;
 
 end; (* local *)