1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 19 00:47:23 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 19 06:14:37 2010 +0100
     1.3 @@ -131,12 +131,12 @@
     1.4  (* produces the rep or abs constant for a qty *)
     1.5  fun absrep_const flag ctxt qty_str =
     1.6  let
     1.7 -  val thy = ProofContext.theory_of ctxt
     1.8    val qty_name = Long_Name.base_name qty_str
     1.9 +  val qualifier = Long_Name.qualifier qty_str
    1.10  in
    1.11    case flag of
    1.12 -    AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
    1.13 -  | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
    1.14 +    AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
    1.15 +  | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
    1.16  end
    1.17  
    1.18  (* Lets Nitpick represent elements of quotient types as elements of the raw type *)