--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 27 13:50:55 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 27 13:52:31 2011 +0200
@@ -553,9 +553,9 @@
if same_const rtrm qtrm then rtrm
else
let
- val rtrm' = #rconst (Quotient_Info.qconsts_lookup thy qtrm)
- handle Quotient_Info.NotFound =>
- term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
+ val rtrm' = case Quotient_Info.qconsts_lookup thy qtrm of
+ SOME qconst_info => #rconst qconst_info
+ | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
in
if Pattern.matches thy (rtrm', rtrm)
then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm