--- 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*)
--- 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) ||