in a local context, also the free variable case needs to be analysed default tip
authorChristian Urban <urbanc@in.tum.de>
Fri Nov 25 00:18:59 2011 +0000 (2011-11-25)
changeset 45628f21eb7073895
parent 45627 a0336f8b6558
child 45629 ef08425dd2d5
child 45637 5f85efcb50c1
in a local context, also the free variable case needs to be analysed default tip
src/HOL/Tools/Quotient/quotient_term.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Nov 24 21:41:58 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Nov 25 00:18:59 2011 +0000
     1.3 @@ -125,7 +125,8 @@
     1.4    let
     1.5      (* FIXME *)
     1.6      fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
     1.7 -      | mk_dummyT _ = error "Expecting abs/rep term to be a constant"     
     1.8 +      | mk_dummyT (Free (c, _)) = Free (c, dummyT)
     1.9 +      | mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable"     
    1.10    in
    1.11      case Quotient_Info.lookup_abs_rep ctxt qty_str of
    1.12        SOME abs_rep =>