# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322180339 0
# Node ID f21eb7073895be7816a47c8befe431898ddef360
# Parent  a0336f8b65587da4d5a5e8fd0c75937fb558f6a9
in a local context, also the free variable case needs to be analysed default tip

diff -r a0336f8b6558 -r f21eb7073895 src/HOL/Tools/Quotient/quotient_term.ML
--- 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 =>