renamed structure ValueParse to Parse_Value;
eliminated old-style structure alias V;

--- a/src/Pure/IsaMakefile	Sat May 15 23:16:32 2010 +0200
+++ b/src/Pure/IsaMakefile	Sat May 15 23:23:45 2010 +0200
@@ -68,15 +68,15 @@
   Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML			\
   Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
   Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML	\
-  Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML Isar/proof.ML	\
-  Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
-  Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
-  Isar/skip_proof.ML Isar/spec_parse.ML Isar/spec_rules.ML		\
-  Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML		\
-  Isar/typedecl.ML Isar/value_parse.ML ML/ml_antiquote.ML		\
-  ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML	\
-  ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
-  ML/ml_thms.ML ML-Systems/install_pp_polyml.ML				\
+  Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML		\
+  Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML		\
+  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
+  Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML			\
+  Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML		\
+  Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML		\
+  ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML	\
+  ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML		\
+  ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
   ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
   Proof/extraction.ML Proof/proof_rewrite_rules.ML			\
   Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\

--- a/src/Pure/Isar/isar_document.ML	Sat May 15 23:16:32 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Sat May 15 23:23:45 2010 +0200
@@ -275,8 +275,6 @@
 
 (** concrete syntax **)
 
-local structure V = ValueParse in
-
 val _ =
   OuterSyntax.internal_command "Isar.define_command"
     (Parse.string -- Parse.string >> (fn (id, text) =>
@@ -296,12 +294,10 @@
 val _ =
   OuterSyntax.internal_command "Isar.edit_document"
     (Parse.string -- Parse.string --
-        V.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
+        Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
       >> (fn ((id, new_id), edits) =>
         Toplevel.position (Position.id_only new_id) o
         Toplevel.imperative (fn () => edit_document id new_id edits)));
 
 end;
 
-end;
-

--- a/src/Pure/Isar/isar_syn.ML	Sat May 15 23:16:32 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat May 15 23:23:45 2010 +0200
@@ -773,7 +773,7 @@
 (* nested commands *)
 
 val props_text =
-  Scan.optional ValueParse.properties [] -- Parse.position Parse.string
+  Scan.optional Parse_Value.properties [] -- Parse.position Parse.string
   >> (fn (props, (str, pos)) =>
       (Position.of_properties (Position.default_properties pos props), str));
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/parse_value.ML	Sat May 15 23:23:45 2010 +0200
@@ -0,0 +1,42 @@
+(*  Title:      Pure/Isar/parse_value.ML
+    Author:     Makarius
+
+Outer syntax parsers for basic ML values.
+*)
+
+signature PARSE_VALUE =
+sig
+  val comma: 'a parser -> 'a parser
+  val equal: 'a parser -> 'a parser
+  val parens: 'a parser -> 'a parser
+  val unit: unit parser
+  val pair: 'a parser -> 'b parser -> ('a * 'b) parser
+  val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
+  val list: 'a parser -> 'a list parser
+  val properties: Properties.T parser
+end;
+
+structure Parse_Value: PARSE_VALUE =
+struct
+
+(* syntax utilities *)
+
+fun comma p = Parse.$$$ "," |-- Parse.!!! p;
+fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
+fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
+
+
+(* tuples *)
+
+val unit = parens (Scan.succeed ());
+fun pair p1 p2 = parens (p1 -- comma p2);
+fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
+
+
+(* lists *)
+
+fun list p = parens (Parse.enum "," p);
+val properties = list (Parse.string -- equal Parse.string);
+
+end;
+

--- a/src/Pure/Isar/value_parse.ML	Sat May 15 23:16:32 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(*  Title:      Pure/Isar/value_parse.ML
-    Author:     Makarius
-
-Outer syntax parsers for basic ML values.
-*)
-
-signature VALUE_PARSE =
-sig
-  val comma: 'a parser -> 'a parser
-  val equal: 'a parser -> 'a parser
-  val parens: 'a parser -> 'a parser
-  val unit: unit parser
-  val pair: 'a parser -> 'b parser -> ('a * 'b) parser
-  val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
-  val list: 'a parser -> 'a list parser
-  val properties: Properties.T parser
-end;
-
-structure ValueParse: VALUE_PARSE =
-struct
-
-(* syntax utilities *)
-
-fun comma p = Parse.$$$ "," |-- Parse.!!! p;
-fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
-fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
-
-
-(* tuples *)
-
-val unit = parens (Scan.succeed ());
-fun pair p1 p2 = parens (p1 -- comma p2);
-fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
-
-
-(* lists *)
-
-fun list p = parens (Parse.enum "," p);
-val properties = list (Parse.string -- equal Parse.string);
-
-end;
-

--- a/src/Pure/ROOT.ML	Sat May 15 23:16:32 2010 +0200
+++ b/src/Pure/ROOT.ML	Sat May 15 23:23:45 2010 +0200
@@ -170,7 +170,7 @@
 use "Isar/outer_lex.ML";
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
-use "Isar/value_parse.ML";
+use "Isar/parse_value.ML";
 use "Isar/args.ML";
 
 (*ML support*)