--- a/Attic/Quot/quotient_typ.ML	Sat Mar 13 13:49:15 2010 +0100
+++ b/Attic/Quot/quotient_typ.ML	Sun Mar 14 11:36:15 2010 +0100
@@ -71,11 +71,10 @@
   val typedef_tac =
      EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
-  Local_Theory.theory_result
-    (Typedef.add_typedef false NONE
+  Typedef.add_typedef false NONE
        (qty_name, vs, mx)
           (typedef_term rel rty lthy)
-             NONE typedef_tac) lthy
+             NONE typedef_tac lthy
 end