# HG changeset patch
# User wenzelm
# Date 1126642783 -7200
# Node ID 5746c9bd4356c006d4929b624435cbeccfa99153
# Parent  ee2bdca144c7177714700101e4688b824bb62512
added name_facts;

diff -r ee2bdca144c7 -r 5746c9bd4356 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue Sep 13 22:19:42 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Tue Sep 13 22:19:43 2005 +0200
@@ -73,6 +73,8 @@
   val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
   val xthm: token list -> (thmref * Attrib.src list) * token list
   val xthms1: token list -> (thmref * Attrib.src list) list * token list
+  val name_facts: token list ->
+    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
   val locale_target: token list -> xstring * token list
   val opt_locale_target: token list -> xstring option * token list
   val locale_expr: token list -> Locale.expr * token list
@@ -314,6 +316,8 @@
 val xthm = (xname -- thm_sel >> NameSelection || xname >> Name) -- opt_attribs;
 val xthms1 = Scan.repeat1 xthm;
 
+val name_facts = and_list1 (opt_thm_name "=" -- xthms1);
+
 
 (* locale elements *)