--- a/src/HOL/Tools/numeral.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/numeral.ML Sat Feb 01 18:42:46 2014 +0100
@@ -71,10 +71,10 @@
let
fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
| dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
- | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
+ | dest_bit _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal bit";
fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
- | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
+ | dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
in if negative then ~ (dest_num t) else dest_num t end;
fun pretty literals _ thm _ _ [(t, _)] =
(Code_Printer.str o print literals o dest_numeral thm) t;