src/HOL/hologic.ML

 
 (* int *)
 
 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 *)
 
 val realT = Type("RealDef.real", []);