--- a/Attic/Quot/quotient_typ.ML	Tue Mar 16 17:20:46 2010 +0100
+++ b/Attic/Quot/quotient_typ.ML	Tue Mar 16 18:02:08 2010 +0100
@@ -1,7 +1,7 @@
-(*  Title:      quotient_typ.thy
+(*  Title:      HOL/Tools/Quotient/quotient_typ.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Definition of a quotient type.
+Definition of a quotient type.
 
 *)
 
@@ -74,11 +74,8 @@
   val typedef_tac =
     EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
-  Local_Theory.theory_result
-  (Typedef.add_typedef_global false NONE
-    (qty_name, vs, mx)
-      (typedef_term rel rty lthy)
-        NONE typedef_tac) lthy
+  Typedef.add_typedef false NONE (qty_name, vs, mx) 
+    (typedef_term rel rty lthy) NONE typedef_tac lthy
 end
 
 
@@ -282,7 +279,12 @@
       Syntax.parse_term lthy1 rel_str
       |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
       |> Syntax.check_term lthy1 
-    val lthy2 = Variable.declare_term rel lthy1 
+    val (newT, lthy2) = lthy1
+      |> Typedecl.typedecl_wrt [rel] (qty_name, vs, mx)
+      ||> Variable.declare_term rel 
+   
+    (*val Type (full_qty_name, type_args) = newT
+    val vs' = map Term.dest_TFree type_args*)
   in
     (((vs, qty_name, mx), (rty, rel)), lthy2)
   end