src/HOL/Library/Numeral_Type.thy

--- a/src/HOL/Library/Numeral_Type.thy	Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Oct 21 00:36:12 2009 +0200
@@ -408,7 +408,7 @@
   in bin_of n end;
 
 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
-      mk_bintype (valOf (Int.fromString str))
+      mk_bintype (the (Int.fromString str))
   | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
 
 in [("_NumeralType", numeral_tr)] end;