# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268562975 -3600
# Node ID 45fb38a2e3f791c5e6b3cfd78a5eb303aebc0b6f
# Parent  04dad9b0136d40eec340dacb0af536ba0f5b2f38
localised the typedef in Attic (requires new Isabelle)

diff -r 04dad9b0136d -r 45fb38a2e3f7 Attic/Quot/quotient_typ.ML
--- 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