# HG changeset patch
# User wenzelm
# Date 1183760102 -7200
# Node ID 55ef4d0bc2503f46aff6758670f4da3915e99eaa
# Parent  0886e5861766806aa566f274ed677c9cc1a9770a
moved General/xml.ML to Tools/xml.ML;
actually use pgml.ML;

diff -r 0886e5861766 -r 55ef4d0bc250 src/Pure/ProofGeneral/pgip_standalone.ML
--- a/src/Pure/ProofGeneral/pgip_standalone.ML	Sat Jul 07 00:15:00 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_standalone.ML	Sat Jul 07 00:15:02 2007 +0200
@@ -29,13 +29,14 @@
 use "General/file.ML";     (* used directly *)
 use "General/buffer.ML";
 use "General/symbol.ML";
-use "General/xml.ML";      (* used directly *)
 use "General/url.ML";      (* used directly *)
+use "Tools/xml.ML";        (* used directly *)
 
 
 (* Our code *)
 
 use "ProofGeneral/pgip_types.ML";
+use "ProofGeneral/pgml.ML";
 use "ProofGeneral/pgip_markup.ML";
 use "ProofGeneral/pgip_input.ML";
 use "ProofGeneral/pgip_output.ML";