# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268975677 -3600
# Node ID 23908b4dbc2fbd70f4cf1640a4a1dda83661a7ae
# Parent  7c170d39a80878911ae29267db1eecfac497b221
Check that argument is not a 'Bound' before calling fastype_of.

diff -r 7c170d39a808 -r 23908b4dbc2f src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Mar 19 00:47:23 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Mar 19 06:14:37 2010 +0100
@@ -289,7 +289,8 @@
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>
     case (try bare_concl goal) of
-      SOME (rel $ _ $ (rep $ (abs $ _))) =>
+      SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
+    | SOME (rel $ _ $ (rep $ (abs $ _))) =>
         let
           val thy = ProofContext.theory_of ctxt;
           val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
diff -r 7c170d39a808 -r 23908b4dbc2f src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 19 00:47:23 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 19 06:14:37 2010 +0100
@@ -131,12 +131,12 @@
 (* produces the rep or abs constant for a qty *)
 fun absrep_const flag ctxt qty_str =
 let
-  val thy = ProofContext.theory_of ctxt
   val qty_name = Long_Name.base_name qty_str
+  val qualifier = Long_Name.qualifier qty_str
 in
   case flag of
-    AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
-  | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
+    AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
+  | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
 end
 
 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)