1.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Aug 26 13:09:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Aug 26 15:48:08 2010 +0200
     1.3 @@ -77,7 +77,8 @@
     1.4    Typedef.add_typedef false NONE (qty_name, vs, mx) 
     1.5      (typedef_term rel rty lthy) NONE typedef_tac lthy
     1.6  *)
     1.7 -   Local_Theory.theory_result
     1.8 +(* FIXME should really use local typedef here *)
     1.9 +   Local_Theory.background_theory_result
    1.10       (Typedef.add_typedef_global false NONE
    1.11         (qty_name, map (rpair dummyS) vs, mx)
    1.12           (typedef_term rel rty lthy)