--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Nov 24 21:41:58 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Nov 25 00:18:59 2011 +0000
@@ -125,7 +125,8 @@
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 =>