thmref: Name vs. NameSelection;
authorwenzelm
Mon Jun 20 22:14:12 2005 +0200 (2005-06-20)
changeset 164989d265401fee0
parent 16497 474472ca4e4d
child 16499 2076b2e6ac58
thmref: Name vs. NameSelection;
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Jun 20 22:14:11 2005 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Jun 20 22:14:12 2005 +0200
     1.3 @@ -158,11 +158,12 @@
     1.4  (* theorems *)
     1.5  
     1.6  fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
     1.7 -  Scan.ahead Args.name -- Args.named_fact (fn name => get st (name, NONE)) --
     1.8 +  Scan.ahead Args.name -- Args.named_fact (fn name => get st (Name name)) --
     1.9    Scan.option Args.thm_sel -- Args.opt_attribs (intern (theory_of st))
    1.10    >> (fn (((name, fact), sel), srcs) =>
    1.11      let
    1.12 -      val ths = PureThy.select_thm (name, sel) fact;
    1.13 +      val thmref = (case sel of NONE => Name name | SOME is => NameSelection (name, is));
    1.14 +      val ths = PureThy.select_thm thmref fact;
    1.15        val atts = map (attrib (theory_of st)) srcs;
    1.16        val (st', ths') = Thm.applys_attributes ((st, ths), atts);
    1.17      in (st', pick name ths') end));
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Jun 20 22:14:11 2005 +0200
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Jun 20 22:14:12 2005 +0200
     2.3 @@ -485,8 +485,8 @@
     2.4              if a <> "" then (j, (a, ths))
     2.5              else if m = n then (j, (name, ths))
     2.6              else if m = 1 then
     2.7 -              (j, (PureThy.string_of_thmref (name, SOME [PureThy.Single i]), ths))
     2.8 -            else (j, (PureThy.string_of_thmref (name, SOME [PureThy.FromTo (i, j - 1)]), ths))
     2.9 +              (j, (PureThy.string_of_thmref (NameSelection (name, [Single i])), ths))
    2.10 +            else (j, (PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths))
    2.11            end;
    2.12        in #2 (foldl_map name_res (1, res)) end;
    2.13  
    2.14 @@ -600,8 +600,8 @@
    2.15  
    2.16  fun method_setup (name, txt, cmt) =
    2.17    Context.use_let
    2.18 -    "val thm = PureThy.get_thm_closure (Context.the_context ());\n\
    2.19 -    \val thms = PureThy.get_thms_closure (Context.the_context ());\n\
    2.20 +    "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
    2.21 +    \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
    2.22      \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
    2.23      "Method.add_method method"
    2.24      ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
     3.1 --- a/src/Pure/Isar/outer_parse.ML	Mon Jun 20 22:14:11 2005 +0200
     3.2 +++ b/src/Pure/Isar/outer_parse.ML	Mon Jun 20 22:14:12 2005 +0200
     3.3 @@ -305,7 +305,7 @@
     3.4    nat --| minus >> PureThy.From ||
     3.5    nat >> PureThy.Single) --| $$$ ")";
     3.6  
     3.7 -val xthm = xname -- Scan.option thm_sel -- opt_attribs;
     3.8 +val xthm = (xname -- thm_sel >> NameSelection || xname >> Name) -- opt_attribs;
     3.9  val xthms1 = Scan.repeat1 xthm;
    3.10  
    3.11