# HG changeset patch
# User berghofe
# Date 1057928190 -7200
# Node ID afd168fdcd3a6cb4cd4bc0975fcf99a53772f080
# Parent  8af7334af4b3bd4f3549a29db9e6e9dc6b9ede10
mk_int now produces specific constants for 0 and 1.

diff -r 8af7334af4b3 -r afd168fdcd3a src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Fri Jul 11 14:55:17 2003 +0200
+++ b/src/HOL/hologic.ML	Fri Jul 11 14:56:30 2003 +0200
@@ -321,7 +321,9 @@
 
 val intT = Type ("IntDef.int", []);
 
-fun mk_int i = number_of_const intT $ mk_bin i;
+fun mk_int 0 = Const ("0", intT)
+  | mk_int 1 = Const ("1", intT)
+  | mk_int i = number_of_const intT $ mk_bin i;
 
 
 (* real *)