diff -r 1e08743b6997 -r a9e55e1ef64c Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Dec 11 16:32:40 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Dec 11 17:19:38 2009 +0100
@@ -31,18 +31,18 @@
 fun get_fun_aux lthy s fs =
   case (maps_lookup (ProofContext.theory_of lthy) s) of
     SOME info => list_comb (Const (#mapfun info, dummyT), fs)
-  | NONE      => raise 
+  | NONE      => raise
         (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
 
 fun get_const flag lthy _ qty =
 (* FIXME: check here that _ and qty are related *)
-let 
+let
   val thy = ProofContext.theory_of lthy
   val qty_name = Long_Name.base_name (fst (dest_Type qty))
 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 (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
+  | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
 
@@ -53,17 +53,17 @@
 
 fun get_fun flag lthy (rty, qty) =
   if rty = qty then mk_identity qty else
-  case (rty, qty) of 
+  case (rty, qty) of
     (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
      let
        val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
        val fs_ty2 = get_fun flag lthy (ty2, ty2')
-     in  
+     in
        get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
-     end 
+     end
   | (Type (s, []), Type (s', [])) =>
      if s = s'
-     then mk_identity qty 
+     then mk_identity qty
      else get_const flag lthy rty qty
   | (Type (s, tys), Type (s', tys')) =>
      if s = s'
@@ -71,7 +71,7 @@
      else get_const flag lthy rty qty
   | (TFree x, TFree x') =>
      if x = x'
-     then mk_identity qty 
+     then mk_identity qty
      else raise (LIFT_MATCH "get_fun")
   | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
   | _ => raise (LIFT_MATCH "get_fun")