# HG changeset patch
# User wenzelm
# Date 1167943022 -3600
# Node ID f3d550d2b145100300a585150a225d9295734602
# Parent  b0c966b3006607344d91e816915c48facaf18ef6
removed obsolete ProofGeneral/syntax_standalone.ML;

diff -r b0c966b30066 -r f3d550d2b145 src/Pure/ProofGeneral/pgip_standalone.ML
--- 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 *)
 
diff -r b0c966b30066 -r f3d550d2b145 src/Pure/ProofGeneral/syntax_standalone.ML
--- 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
-