--- a/src/HOL/Integ/Bin.thy Fri Sep 25 13:18:07 1998 +0200
+++ b/src/HOL/Integ/Bin.thy Fri Sep 25 13:57:01 1998 +0200
@@ -22,7 +22,7 @@
quoting the previously computed values. (Or code an oracle...)
*)
-Bin = Integ + Datatype +
+Bin = Int + Datatype +
syntax
"_Int" :: xnum => int ("_")