src/HOL/Library/sct.ML

--- a/src/HOL/Library/sct.ML	Tue Sep 18 11:06:22 2007 +0200
+++ b/src/HOL/Library/sct.ML	Tue Sep 18 16:08:00 2007 +0200
@@ -157,8 +157,8 @@
       measures
     end
 
-val mk_number = HOLogic.mk_nat o IntInf.fromInt
-val dest_number = IntInf.toInt o HOLogic.dest_nat
+val mk_number = HOLogic.mk_nat
+val dest_number = HOLogic.dest_nat
 
 fun nums_to i = map mk_number (0 upto (i - 1))