src/HOL/Tools/Quotient/quotient_term.ML

 (* produces the rep or abs constant for a qty *)
 fun absrep_const flag ctxt qty_str =
   let
     (* FIXME *)
     fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
-      | mk_dummyT _ = error "Expecting abs/rep term to be a constant"     
+      | mk_dummyT (Free (c, _)) = Free (c, dummyT)
+      | mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable"     
   in
     case Quotient_Info.lookup_abs_rep ctxt qty_str of
       SOME abs_rep => 
         mk_dummyT (case flag of
           AbsF => #abs abs_rep