always refine interpretation morphism using canonical constant's definition theorem

--- a/src/Pure/Isar/class.ML	Wed Jun 04 15:32:25 2014 +0200
+++ b/src/Pure/Isar/class.ML	Thu Jun 05 10:52:19 2014 +0200
@@ -227,7 +227,7 @@
         (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
   | NONE => thy);
 
-fun register_operation class (c, (t, some_def)) thy =
+fun register_operation class (c, t) thy =
   let
     val base_sort = base_sort thy class;
     val prep_typ = map_type_tfree
@@ -237,11 +237,18 @@
     val ty' = Term.fastype_of t';
   in
     thy
-    |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd)
-      (fn (defs, operations) =>
-        (fold cons (the_list some_def) defs,
-          (c, (class, (ty', t'))) :: operations))
-    |> activate_defs class (the_list some_def)
+    |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apsnd)
+        (cons (c, (class, (ty', t'))))
+  end;
+
+fun register_def class def_thm thy =
+  let
+    val sym_thm = Thm.symmetric def_thm
+  in
+    thy
+    |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apfst)
+        (cons sym_thm)
+    |> activate_defs class [sym_thm]
   end;
 
 
@@ -362,8 +369,8 @@
     |> Sign.declare_const_global ((b, Type.strip_sorts ty), mx)
     |> snd
     |> global_def (b_def, def_eq)
-    |-> (fn def_thm =>
-      null dangling_params ? register_operation class (c, (rhs, SOME (Thm.symmetric def_thm))))
+    |-> (fn def_thm => register_def class def_thm)
+    |> null dangling_params ? register_operation class (c, rhs)
     |> Sign.add_const_constraint (c, SOME ty)
   end;
 
@@ -379,7 +386,7 @@
     |> snd
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
     |> (null dangling_term_params andalso not (#1 prmode = Print_Mode.input))
-      ? register_operation class (c', (rhs', NONE))
+      ? register_operation class (c', rhs')
     |> Sign.add_const_constraint (c', SOME ty')
   end;