# HG changeset patch
# User kleing
# Date 1082359647 -7200
# Node ID 1ef710003a35b719e14af2cdc739a2fde64a45ca
# Parent  9b3397a848c3f6379bc1547817989e42483627b4
change quote to Library.quote, fixes LaTeX \isarchardoublequote problem.

diff -r 9b3397a848c3 -r 1ef710003a35 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Apr 19 08:20:52 2004 +0200
+++ b/src/Pure/Isar/args.ML	Mon Apr 19 09:27:27 2004 +0200
@@ -72,12 +72,12 @@
 fun pos_of (Arg (_, (_, pos))) = pos;
 
 fun str_of (Arg (Ident, (x, _))) = x
-  | str_of (Arg (String, (x, _))) = quote x
+  | str_of (Arg (String, (x, _))) = Library.quote x
   | str_of (Arg (Keyword, (x, _))) = x
   | str_of (Arg (EOF, _)) = "end-of-text";
 
 fun string_of (Arg (Ident, (x, _))) = x
-  | string_of (Arg (String, (x, _))) = quote x
+  | string_of (Arg (String, (x, _))) = Library.quote x
   | string_of (Arg (Keyword, (x, _))) = x
   | string_of (Arg (EOF, _)) = "";
 
@@ -229,7 +229,7 @@
 fun err_in_src kind msg (Src ((s, args), pos)) =
   error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
     space_implode " " (map str_of args));
-
+    
 
 (* argument syntax *)