# HG changeset patch
# User wenzelm
# Date 1119298452 -7200
# Node ID 9d265401fee01ab9f01d9ad0f4c1aa2b27a9281d
# Parent  474472ca4e4dff0517addccdaa70ed786935dce7
thmref: Name vs. NameSelection;

diff -r 474472ca4e4d -r 9d265401fee0 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Jun 20 22:14:11 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Jun 20 22:14:12 2005 +0200
@@ -158,11 +158,12 @@
 (* theorems *)
 
 fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
-  Scan.ahead Args.name -- Args.named_fact (fn name => get st (name, NONE)) --
+  Scan.ahead Args.name -- Args.named_fact (fn name => get st (Name name)) --
   Scan.option Args.thm_sel -- Args.opt_attribs (intern (theory_of st))
   >> (fn (((name, fact), sel), srcs) =>
     let
-      val ths = PureThy.select_thm (name, sel) fact;
+      val thmref = (case sel of NONE => Name name | SOME is => NameSelection (name, is));
+      val ths = PureThy.select_thm thmref fact;
       val atts = map (attrib (theory_of st)) srcs;
       val (st', ths') = Thm.applys_attributes ((st, ths), atts);
     in (st', pick name ths') end));
diff -r 474472ca4e4d -r 9d265401fee0 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Mon Jun 20 22:14:11 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Mon Jun 20 22:14:12 2005 +0200
@@ -485,8 +485,8 @@
             if a <> "" then (j, (a, ths))
             else if m = n then (j, (name, ths))
             else if m = 1 then
-              (j, (PureThy.string_of_thmref (name, SOME [PureThy.Single i]), ths))
-            else (j, (PureThy.string_of_thmref (name, SOME [PureThy.FromTo (i, j - 1)]), ths))
+              (j, (PureThy.string_of_thmref (NameSelection (name, [Single i])), ths))
+            else (j, (PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths))
           end;
       in #2 (foldl_map name_res (1, res)) end;
 
@@ -600,8 +600,8 @@
 
 fun method_setup (name, txt, cmt) =
   Context.use_let
-    "val thm = PureThy.get_thm_closure (Context.the_context ());\n\
-    \val thms = PureThy.get_thms_closure (Context.the_context ());\n\
+    "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
+    \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
     \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
     "Method.add_method method"
     ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
diff -r 474472ca4e4d -r 9d265401fee0 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Mon Jun 20 22:14:11 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Mon Jun 20 22:14:12 2005 +0200
@@ -305,7 +305,7 @@
   nat --| minus >> PureThy.From ||
   nat >> PureThy.Single) --| $$$ ")";
 
-val xthm = xname -- Scan.option thm_sel -- opt_attribs;
+val xthm = (xname -- thm_sel >> NameSelection || xname >> Name) -- opt_attribs;
 val xthms1 = Scan.repeat1 xthm;