diff -r 88cab786d024 -r df3252bbc0e6 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Thu Aug 17 09:24:50 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Thu Aug 17 09:24:51 2006 +0200
@@ -410,11 +410,11 @@
      of [] => ()
       | dupl_tycos => error ("type constructors occur more than once in arities: "
         ^ (commas o map quote) dupl_tycos);
-    val name = case raw_name
-     of "" => Thm.def_name ((space_implode "_" o map NameSpace.base)
+    val (bind_always, name) = case raw_name
+     of "" => (false, Thm.def_name ((space_implode "_" o map NameSpace.base)
                 (maps (fn (tyco, _, sort) => sort @ [tyco])
-                (sort (fn ((tyco1, _, _), (tyco2, _, _)) => string_ord (tyco1, tyco2)) arities)))
-      | _ => raw_name;
+                (sort (fn ((tyco1, _, _), (tyco2, _, _)) => string_ord (tyco1, tyco2)) arities))))
+      | _ => (true, raw_name);
     val atts = map (prep_att theory) raw_atts;
     fun already_defined (c, ty_inst) = 
       is_some (find_first (fn (_, { lhs = [ty_inst'], ...}) =>
@@ -473,13 +473,16 @@
     fun note_all thy =
       (*FIXME: should avoid binding duplicated names*)
       let
+        val bind = bind_always orelse not (can (PureThy.get_thms thy) (Name name));
         val thms = maps (fn (tyco, _, sort) => maps (fn class =>
           Symtab.lookup_list
             ((snd o the_class_data thy) class) tyco) (the_ancestry thy sort)) arities;
-      in
+      in if bind then
         thy
         |> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])]
         |> snd
+      else
+        thy
       end;
     fun after_qed cs thy =
       thy
@@ -567,7 +570,7 @@
 
 type sortcontext = (string * sort) list;
 
-fun sortcontext_of_typ thy ty = fold_atyps
+fun sortcontext_of_typ thy ty = (rev ooo fold_atyps)
   (fn TFree (v, S) =>
     (case operational_sort_of thy S of
       [] => I