1.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Mar 19 00:47:23 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Mar 19 06:14:37 2010 +0100
     1.3 @@ -289,7 +289,8 @@
     1.4  fun rep_abs_rsp_tac ctxt =
     1.5    SUBGOAL (fn (goal, i) =>
     1.6      case (try bare_concl goal) of
     1.7 -      SOME (rel $ _ $ (rep $ (abs $ _))) =>
     1.8 +      SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
     1.9 +    | SOME (rel $ _ $ (rep $ (abs $ _))) =>
    1.10          let
    1.11            val thy = ProofContext.theory_of ctxt;
    1.12            val (ty_a, ty_b) = dest_fun_type (fastype_of abs);

     2.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 19 00:47:23 2010 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 19 06:14:37 2010 +0100
     2.3 @@ -131,12 +131,12 @@
     2.4  (* produces the rep or abs constant for a qty *)
     2.5  fun absrep_const flag ctxt qty_str =
     2.6  let
     2.7 -  val thy = ProofContext.theory_of ctxt
     2.8    val qty_name = Long_Name.base_name qty_str
     2.9 +  val qualifier = Long_Name.qualifier qty_str
    2.10  in
    2.11    case flag of
    2.12 -    AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
    2.13 -  | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
    2.14 +    AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
    2.15 +  | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
    2.16  end
    2.17  
    2.18  (* Lets Nitpick represent elements of quotient types as elements of the raw type *)