diff -r 1c4a8d3b26d2 -r a814cccce0b8 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Tue Mar 16 06:55:01 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Tue Mar 16 08:45: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,8 +74,17 @@
   val typedef_tac =
     EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
+(* FIXME: purely local typedef causes at the moment 
+   problems with type variables
+  
   Typedef.add_typedef false NONE (qty_name, vs, mx) 
     (typedef_term rel rty lthy) NONE typedef_tac lthy
+*)
+   Local_Theory.theory_result
+     (Typedef.add_typedef_global false NONE
+       (qty_name, vs, mx)
+         (typedef_term rel rty lthy)
+           NONE typedef_tac) lthy
 end