# HG changeset patch
# User wenzelm
# Date 1218737622 -7200
# Node ID af9f0adbab1fb7e0cfeaa966ae1e175647bc2f77
# Parent  4b79407825dab5a8c8f6b124bc2dda9b4e893b03
renamed P.ml_source to P.ML_source;

diff -r 4b79407825da -r af9f0adbab1f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Aug 14 20:13:41 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 14 20:13:42 2008 +0200
@@ -299,40 +299,40 @@
 
 val _ =
   OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.thy_decl)
-    (P.ml_source >> (fn (txt, pos) =>
+    (P.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
 
 val _ =
   OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
-    (P.ml_source >> IsarCmd.ml_diag true);
+    (P.ML_source >> IsarCmd.ml_diag true);
 
 val _ =
   OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
-    (P.ml_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
+    (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
 
 val _ =
   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
-    (P.ml_source >> (Toplevel.theory o IsarCmd.generic_setup));
+    (P.ML_source >> (Toplevel.theory o IsarCmd.generic_setup));
 
 val _ =
   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
-    (P.name -- P.!!! (P.$$$ "=" |-- P.ml_source -- P.text)
+    (P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
     >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
   OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
-    (P.ml_source >> IsarCmd.declaration);
+    (P.ML_source >> IsarCmd.declaration);
 
 val _ =
   OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
     (P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
-      P.ml_source -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
+      P.ML_source -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
     >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
 
 
 (* translation functions *)
 
-val trfun = P.opt_keyword "advanced" -- P.ml_source;
+val trfun = P.opt_keyword "advanced" -- P.ML_source;
 
 val _ =
   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
@@ -364,8 +364,8 @@
 
 val _ =
   OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
-    (P.name -- (P.$$$ "(" |-- P.ml_source --| P.$$$ ")" --| P.$$$ "=")
-      -- P.ml_source >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
+    (P.name -- (P.$$$ "(" |-- P.ML_source --| P.$$$ ")" --| P.$$$ "=")
+      -- P.ML_source >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
 
 
 (* local theories *)
diff -r 4b79407825da -r af9f0adbab1f src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Aug 14 20:13:41 2008 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Thu Aug 14 20:13:42 2008 +0200
@@ -85,7 +85,7 @@
   val fixes: token list -> (string * string option * mixfix) list * token list
   val for_fixes: token list -> (string * string option * mixfix) list * token list
   val for_simple_fixes: token list -> (string * string option) list * token list
-  val ml_source: token list -> (SymbolPos.text * Position.T) * token list
+  val ML_source: token list -> (SymbolPos.text * Position.T) * token list
   val doc_source: token list -> (SymbolPos.text * Position.T) * token list
   val term_group: token list -> string * token list
   val prop_group: token list -> string * token list
@@ -302,9 +302,9 @@
 val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
 
 
-(* embedded text *)
+(* embedded source text *)
 
-val ml_source = source_position (group "ML source" text);
+val ML_source = source_position (group "ML source" text);
 val doc_source = source_position (group "document source" text);