--- a/src/Pure/ProofGeneral/pgip_standalone.ML Thu Jan 04 21:36:52 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_standalone.ML Thu Jan 04 21:37:02 2007 +0100
@@ -28,8 +28,6 @@
use "General/xml.ML"; (* used directly *)
use "General/url.ML"; (* used directly *)
-use "ProofGeneral/syntax_standalone.ML";
-
(* Our code *)
--- a/src/Pure/ProofGeneral/syntax_standalone.ML Thu Jan 04 21:36:52 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Taken from ../Syntax/lexicon.ML, which otherwise pulls in whole
- term structure of Isabelle
-*)
-signature SYNTAX =
-sig
- val read_int: string -> int option
- val read_nat: string -> int option
-end
-
-structure Syntax : SYNTAX =
-struct
-
-local
-
-val scan_digits1 = Scan.many1 Symbol.is_digit;
-
-fun nat cs =
- Option.map (#1 o Library.read_int)
- (Scan.read Symbol.stopper scan_digits1 cs);
-
-in
-
-val read_nat = nat o Symbol.explode;
-
-fun read_int s =
- (case Symbol.explode s of
- "-" :: cs => Option.map ~ (nat cs)
- | cs => nat cs);
-
-end;
-
-end
-