src/HOL/Tools/Quotient/quotient_term.ML
changeset 45274 252cd58847e0
parent 45273 728ed9d28c63
child 45279 89a17197cb98
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:50:55 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Oct 27 13:52:31 2011 +0200
     1.3 @@ -553,9 +553,9 @@
     1.4          if same_const rtrm qtrm then rtrm
     1.5          else
     1.6            let
     1.7 -            val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm)
     1.8 -              handle Quotient_Info.NotFound =>
     1.9 -                term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
    1.10 +            val rtrm' = case Quotient_Info.qconsts_lookup thy qtrm of
    1.11 +              SOME qconst_info => #rconst qconst_info
    1.12 +            | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
    1.13            in
    1.14              if Pattern.matches thy (rtrm', rtrm)
    1.15              then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm