# HG changeset patch
# User wenzelm
# Date 1085835524 -7200
# Node ID 4dae1cb304a4e89c5e183294ea479d4d704e40bc
# Parent  ad83019a66a4b2165e75892be844465b8324ba6b
Library.read_int;

diff -r ad83019a66a4 -r 4dae1cb304a4 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sat May 29 14:57:39 2004 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Sat May 29 14:58:44 2004 +0200
@@ -118,7 +118,7 @@
       HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
     val goal = mk_nonempty set;
     val vname = take_suffix Symbol.is_digit (Symbol.explode name)
-      |> apfst implode |> apsnd (#1 o Term.read_int);
+      |> apfst implode |> apsnd (#1 o Library.read_int);
     val goal_pat = mk_nonempty (Var (vname, setT));
 
     (*lhs*)
diff -r ad83019a66a4 -r 4dae1cb304a4 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Sat May 29 14:57:39 2004 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Sat May 29 14:58:44 2004 +0200
@@ -192,10 +192,13 @@
     $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
     Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
 
+  fun read_int ["0", "0"] = ~1
+    | read_int cs = #1 (Library.read_int cs);
+
   val scan_sym =
     $$ "_" >> K (Argument ("", 0)) ||
     $$ "\\<index>" >> K index ||
-    $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o #1 o Term.read_int) ||
+    $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
     $$ ")" >> K En ||
     $$ "/" -- $$ "/" >> K (Brk ~1) ||
     $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||