# HG changeset patch
# User wenzelm
# Date 1208360440 -7200
# Node ID 0701201def955b5b3ca9d35ac965bf84cb3f738d
# Parent  8492816588594a4730c8dcd5e6f733c11966b28d
tuned;

diff -r 849281658859 -r 0701201def95 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Wed Apr 16 17:40:39 2008 +0200
+++ b/src/Pure/General/yxml.ML	Wed Apr 16 17:40:40 2008 +0200
@@ -101,7 +101,7 @@
 (* parsing *)
 
 fun parse_attrib s =
-  (case String.fields (is_char "=") s of
+  (case space_explode "=" s of
     [] => err_attribute ()
   | "" :: _ => err_attribute ()
   | a :: xs => (a, space_implode "=" xs));
diff -r 849281658859 -r 0701201def95 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Apr 16 17:40:39 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 16 17:40:40 2008 +0200
@@ -835,11 +835,13 @@
   fn x => pretty_arity ctxt x);
 
 (*educated guess for reconstructing infixes*)
-fun guess_infix (Syntax (syn, _)) c = case Parser.guess_infix_lr (#gram syn) c
- of SOME (s, l, r, j) => SOME (if l then Mixfix.InfixlName (s, j)
+fun guess_infix (Syntax ({gram, ...}, _)) c =
+  (case Parser.guess_infix_lr gram c of
+    SOME (s, l, r, j) => SOME
+     (if l then Mixfix.InfixlName (s, j)
       else if r then Mixfix.InfixrName (s, j)
       else Mixfix.InfixName (s, j))
-  | NONE => NONE
+  | NONE => NONE);
 
 (*export parts of internal Syntax structures*)
 open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
@@ -849,11 +851,10 @@
 structure BasicSyntax: BASIC_SYNTAX = Syntax;
 open BasicSyntax;
 
-structure Hidden = struct end;
-structure Ast = Hidden;
-structure SynExt = Hidden;
-structure Parser = Hidden;
-structure TypeExt = Hidden;
-structure SynTrans = Hidden;
-structure Mixfix = Hidden;
-structure Printer = Hidden;
+forget_structure "Ast";
+forget_structure "SynExt";
+forget_structure "Parser";
+forget_structure "TypeExt";
+forget_structure "SynTrans";
+forget_structure "Mixfix";
+forget_structure "Printer";