# HG changeset patch
# User wenzelm
# Date 1014666687 -3600
# Node ID 48fbe245879e90a573c7137dae3c8a80b593cceb
# Parent  8a1147c57575c4e85ff786218377d90349a58d44
export locale_target, locale_keyword;

diff -r 8a1147c57575 -r 48fbe245879e src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Mon Feb 25 20:51:00 2002 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Mon Feb 25 20:51:27 2002 +0100
@@ -68,7 +68,9 @@
   val spec_opt_name: token list -> ((bstring * string) * Args.src list) * token list
   val xthm: token list -> (xstring * Args.src list) * token list
   val xthms1: token list -> (xstring * Args.src list) list * token list
+  val locale_target: token list -> xstring option * token list
   val locale_expr: token list -> Locale.expr * token list
+  val locale_keyword: token list -> string * token list
   val locale_element: token list -> Args.src Locale.element * token list
   val method: token list -> Method.text * token list
 end;
@@ -309,7 +311,9 @@
 
 in
 
+val locale_target = Scan.option (($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")"));
 val locale_expr = expr0;
+val locale_keyword = loc_keyword;
 
 val locale_element = group "locale element"
   ($$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix