diff -r c1836b14c63a -r 8a5412121687 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Mar 09 08:45:55 2007 +0100
@@ -150,14 +150,16 @@
            (*rhs' == rhs*)   Thm.symmetric rhs_conv];
         val lthy4 = case some_class
          of SOME class => 
-              LocalTheory.raw_theory
+              lthy3
+              |> LocalTheory.raw_theory
                 (ClassPackage.add_def_in_class lthy3 class
-                  ((c, mx), ((name, atts), (rhs, eq)))) lthy3
+                  ((c, mx), ((name, atts), (rhs, eq))))
           | _ => lthy3;
       in ((lhs, ((name', atts), [([eq], [])])), lthy4) end;
 
     val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
     val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
+
   in (lhss ~~ map (apsnd the_single) res, lthy'') end;
 
 end;