# HG changeset patch
# User wenzelm
# Date 1085836002 -7200
# Node ID 695ee8ad0bb6fc30163d88347689107db5b42ca0
# Parent  e47744683560e0b81a6d798f28538e32a520defb
Library.read_int; Output.output;

diff -r e47744683560 -r 695ee8ad0bb6 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Sat May 29 15:06:19 2004 +0200
+++ b/src/Pure/Isar/isar_output.ML	Sat May 29 15:06:42 2004 +0200
@@ -97,7 +97,7 @@
 fun integer s =
   let
     fun int ss =
-      (case Term.read_int ss of (i, []) => i | _ => error ("Bad integer value: " ^ quote s));
+      (case Library.read_int ss of (i, []) => i | _ => error ("Bad integer value: " ^ quote s));
   in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
 
 
@@ -282,20 +282,20 @@
 
 fun cond_display prt =
   if ! display then
-    Pretty.string_of (Pretty.indent (! indent) prt)
+    Output.output (Pretty.string_of (Pretty.indent (! indent) prt))
     |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
-    (if ! break then Pretty.string_of else Pretty.str_of) prt
+    Output.output ((if ! break then Pretty.string_of else Pretty.str_of) prt)
     |> enclose "\\isa{" "}";
 
 fun cond_seq_display prts =
   if ! display then
-    map (Pretty.string_of o Pretty.indent (! indent)) prts
+    map (Output.output o Pretty.string_of o Pretty.indent (! indent)) prts
     |> separate "\\isasep\\isanewline%\n"
     |> implode
     |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
-    map (if ! break then Pretty.string_of else Pretty.str_of) prts
+    map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of)) prts
     |> separate "\\isasep\\isanewline%\n"
     |> implode
     |> enclose "\\isa{" "}";
diff -r e47744683560 -r 695ee8ad0bb6 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sat May 29 15:06:19 2004 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sat May 29 15:06:42 2004 +0200
@@ -149,7 +149,7 @@
 
 val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
 
-val nat = number >> (fst o Term.read_int o Symbol.explode);
+val nat = number >> (#1 o Library.read_int o Symbol.explode);
 
 val not_eof = Scan.one T.not_eof;
 
diff -r e47744683560 -r 695ee8ad0bb6 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat May 29 15:06:19 2004 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat May 29 15:06:42 2004 +0200
@@ -360,7 +360,7 @@
 (* read_nat *)
 
 fun read_nat str =
-  apsome (#1 o Term.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
+  apsome (#1 o Library.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
 
 
 (* read_xnum *)
@@ -373,7 +373,7 @@
       | "#" :: cs => (1, cs)
       | "-" :: cs => (~1, cs)
       | cs => (1, cs));
-  in sign * #1 (Term.read_int digs) end;
+  in sign * #1 (Library.read_int digs) end;
 
 
 (* read_ident(s) *)