# HG changeset patch
# User wenzelm
# Date 1408699879 -7200
# Node ID b2b93903ab6b5108d5fcf22066f91275c52755d0
# Parent  62826b36ac5e1c0bc5dcb04a8d417618ad39a6d7# Parent  c6b131e651e68892754b6be1cf9dddcf12c6f50b
merged

diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -221,15 +221,15 @@
 val _ =
   Outer_Syntax.local_theory @{command_spec "case_of_simps"}
     "turn a list of equations into a case expression"
-    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthms1 >> case_of_simps_cmd)
+    (Parse_Spec.opt_thm_name ":"  -- Parse.xthms1 >> case_of_simps_cmd)
 
 val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--
-  Parse_Spec.xthms1 --| @{keyword ")"}
+  Parse.xthms1 --| @{keyword ")"}
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "simps_of_case"}
     "perform case split on rule"
-    (Parse_Spec.opt_thm_name ":"  -- Parse_Spec.xthm --
+    (Parse_Spec.opt_thm_name ":"  -- Parse.xthm --
       Scan.optional parse_splits [] >> simps_of_case_cmd)
 
 end
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -525,7 +525,7 @@
     fun do_method named_thms ctxt =
       let
         val ref_of_str =
-          suffix ";" #> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none #> Parse_Spec.xthm
+          suffix ";" #> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none #> Parse.xthm
           #> fst
         val thms = named_thms |> maps snd
         val facts = named_thms |> map (ref_of_str o fst o fst)
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -700,7 +700,7 @@
 val liftdef_parser =
   (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
     --| @{keyword "is"} -- Parse.term -- 
-      Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthms1) []) >> Parse.triple1
+      Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
     "definition for constants over the quotient type"
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -796,8 +796,8 @@
 val _ = 
   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     "setup lifting infrastructure" 
-      (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm 
-      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >> 
+      (opt_gen_code -- Parse.xthm -- Scan.option Parse.xthm 
+      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
         (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => 
           setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
 
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -343,7 +343,7 @@
       Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
         (@{keyword "/"} |-- (partial -- Parse.term))  --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
-          -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm)
+          -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -379,7 +379,7 @@
 val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)
 val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
-val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
+val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.xthm)
 val parse_fact_override_chunk =
   (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
   || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -136,7 +136,7 @@
     |> Symbol.source
     |> Token.source {do_recover = SOME false} lex Position.start
     |> Token.source_proper
-    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+    |> Source.source Token.stopper (Parse.xthms1 >> get) NONE
     |> Source.exhaust
   end
 
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -1157,7 +1157,7 @@
 fun gen_ind_decl mk_def coind =
   Parse.fixes -- Parse.for_fixes --
   Scan.optional Parse_Spec.where_alt_specs [] --
-  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) []
+  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) []
   >> (fn (((preds, params), specs), monos) =>
       (snd o gen_add_inductive mk_def true coind preds params specs monos));
 
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Tools/recdef.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -309,7 +309,7 @@
 val defer_recdef_decl =
   Parse.name -- Scan.repeat1 Parse.prop --
   Scan.optional
-    (@{keyword "("} |-- @{keyword "congs"} |-- Parse.!!! (Parse_Spec.xthms1 --| @{keyword ")"})) []
+    (@{keyword "("} |-- @{keyword "congs"} |-- Parse.!!! (Parse.xthms1 --| @{keyword ")"})) []
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
 val _ =
diff -r 62826b36ac5e -r b2b93903ab6b src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/HOL/Tools/try0.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -176,7 +176,7 @@
   implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
 
 val parse_fact_refs =
-  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));
+  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
 
 val parse_attr =
   Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn ss => (ss, [], [], []))
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -45,10 +45,12 @@
     local_theory -> local_theory
   val internal: (morphism -> attribute) -> Token.src
   val add_del: attribute -> attribute -> attribute context_parser
-  val thm_sel: Facts.interval list parser
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
+  val transform_facts: morphism ->
+    (Attrib.binding * (thm list * Token.src list) list) list ->
+    (Attrib.binding * (thm list * Token.src list) list) list
   val partial_evaluation: Proof.context ->
     (binding * (thm list * Token.src list) list) list ->
     (binding * (thm list * Token.src list) list) list
@@ -214,7 +216,9 @@
 
 (* internal attribute *)
 
-fun internal att = Token.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
+fun internal att =
+  Token.src ("Pure.attribute", Position.none)
+    [Token.make_value "<attribute>" (Token.Attribute att)];
 
 val _ = Theory.setup
   (setup (Binding.make ("attribute", @{here}))
@@ -230,11 +234,6 @@
 
 (** parsing attributed theorems **)
 
-val thm_sel = Parse.$$$ "(" |-- Parse.list1
- (Parse.nat --| Parse.minus -- Parse.nat >> Facts.FromTo ||
-  Parse.nat --| Parse.minus >> Facts.From ||
-  Parse.nat >> Facts.Single) --| Parse.$$$ ")";
-
 local
 
 val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
@@ -255,9 +254,10 @@
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
       >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
-     Scan.ahead (Parse.position fact_name -- Scan.option thm_sel) :|-- (fn ((name, pos), sel) =>
-      Args.named_fact (get_named (is_some sel) pos) --| Scan.option thm_sel
-        >> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))
+     Scan.ahead (Parse.position fact_name -- Scan.option Parse.thm_sel) :|--
+      (fn ((name, pos), sel) =>
+        Args.named_fact (get_named (is_some sel) pos) --| Scan.option Parse.thm_sel
+          >> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))
     -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
       let
         val ths = Facts.select thmref fact;
@@ -276,6 +276,13 @@
 end;
 
 
+(* transform fact expressions *)
+
+fun transform_facts phi = map (fn ((a, atts), bs) =>
+  ((Morphism.binding phi a, map (Token.transform_src phi) atts),
+    bs |> map (fn (ths, btts) => (Morphism.fact phi ths, map (Token.transform_src phi) btts))));
+
+
 
 (** partial evaluation -- observing rule/declaration/mixed attributes **)
 
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -201,7 +201,7 @@
 (* outer syntax *)
 
 val calc_args =
-  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
+  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
 
 val _ =
   Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/element.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -26,9 +26,6 @@
   val map_ctxt_attrib: (Token.src -> Token.src) ->
     ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
   val transform_ctxt: morphism -> context_i -> context_i
-  val transform_facts: morphism ->
-    (Attrib.binding * (thm list * Token.src list) list) list ->
-    (Attrib.binding * (thm list * Token.src list) list) list
   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
@@ -105,9 +102,6 @@
   fact = Morphism.fact phi,
   attrib = Token.transform_src phi};
 
-fun transform_facts phi facts =
-  Notes ("", facts) |> transform_ctxt phi |> (fn Notes (_, facts') => facts');
-
 
 
 (** pretty printing **)
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -66,7 +66,7 @@
 (** notes **)
 
 fun standard_facts lthy ctxt =
-  Element.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+  Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
 
 fun standard_notes pred kind facts lthy =
   Local_Theory.map_contexts (fn level => fn ctxt =>
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -228,7 +228,7 @@
 
 val _ =
   Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
-    (Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
+    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
       >> (fn (facts, fixes) =>
           #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
 
@@ -398,7 +398,7 @@
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "bundle"} "define bundle of declarations"
-    ((Parse.binding --| @{keyword "="}) -- Parse_Spec.xthms1 -- Parse.for_fixes
+    ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes
       >> (uncurry Bundle.bundle_cmd));
 
 val _ =
@@ -567,7 +567,7 @@
 
 (* facts *)
 
-val facts = Parse.and_list1 Parse_Spec.xthms1;
+val facts = Parse.and_list1 Parse.xthms1;
 
 val _ =
   Outer_Syntax.command @{command_spec "then"} "forward chaining"
@@ -640,7 +640,7 @@
     ((@{keyword "("} |--
       Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
         --| @{keyword ")"}) ||
-      Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
+      Parse.position Parse.xname >> rpair []) -- Parse.opt_attribs >> (fn ((c, xs), atts) =>
         Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
 
 
@@ -920,19 +920,19 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_statement"}
     "print theorems as long statements"
-    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_stmts);
+    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
-    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_thms);
+    (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
-    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs false);
+    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
-    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs true);
+    (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true);
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -578,7 +578,7 @@
           (* Registrations *)
           (fn thy =>
             fold_rev (fn (_, morph) =>
-              snd o Attrib.global_notes kind (Element.transform_facts morph facts))
+              snd o Attrib.global_notes kind (Attrib.transform_facts morph facts))
             (registrations_of (Context.Theory thy) loc) thy));
 
 
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/method.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -68,8 +68,8 @@
   val method_cmd: Proof.context -> Token.src -> Proof.context -> method
   val evaluate: text -> Proof.context -> method
   type modifier = (Proof.context -> Proof.context) * attribute
-  val section: modifier parser list -> thm list context_parser
-  val sections: modifier parser list -> thm list list context_parser
+  val section: modifier parser list -> declaration context_parser
+  val sections: modifier parser list -> declaration list context_parser
   type text_range = text * Position.range
   val text: text_range option -> text option
   val position: text_range option -> Position.T
@@ -87,8 +87,8 @@
 
 type method = thm list -> cases_tactic;
 
-fun METHOD_CASES tac facts = Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
-fun METHOD tac facts = NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
+fun METHOD_CASES tac : method = fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
+fun METHOD tac : method = fn facts => NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
 
 val fail = METHOD (K no_tac);
 val succeed = METHOD (K all_tac);
@@ -280,7 +280,7 @@
       let
         val context' = context |>
           ML_Context.expression (#pos source)
-            "fun tactic (morphism: morphism) (facts: thm list) : tactic"
+            "fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic"
             "Method.set_tactic tactic" (ML_Lex.read_source false source);
         val tac = the_tactic context';
       in
@@ -392,7 +392,7 @@
 
 fun method_closure ctxt0 src0 =
   let
-    val (src1, meth) = check_src ctxt0 src0;
+    val (src1, _) = check_src ctxt0 src0;
     val src2 = Token.init_assignable_src src1;
     val ctxt = Context_Position.not_really ctxt0;
     val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
@@ -454,15 +454,40 @@
 
 local
 
-fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
-fun app (f, att) ths context = fold_map (Thm.apply_attribute att) ths (Context.map_proof f context);
+fun sect modifier = Scan.depend (fn context =>
+  let
+    val ctxt = Context.proof_of context;
+    fun prep_att src =
+      let
+        val src' = Attrib.check_src ctxt src;
+        val _ = List.app (Token.assign NONE) (Token.args_of_src src');
+      in src' end;
+    val parse_thm =
+      Parse.xthm >> (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs));
+  in
+    Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier parse_thm) >>
+      (fn ((tok, (init, att)), thms) =>
+        let
+          val decl =
+            (case Token.get_value tok of
+              SOME (Token.Declaration decl) => decl
+            | _ =>
+                let
+                  val facts =
+                    Attrib.partial_evaluation ctxt
+                      [((Binding.empty, [Attrib.internal (K att)]), thms)];
+                  fun decl phi =
+                    Context.mapping I init #>
+                    Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
+                  val _ = Token.assign (SOME (Token.Declaration decl)) tok;
+                in decl end);
+        in (Morphism.form decl context, decl) end)
+  end);
 
 in
 
-fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
-  (fn (m, ths) => Scan.succeed (swap (app m ths context))));
-
-fun sections ss = Scan.repeat (section ss);
+val section = sect o Scan.first;
+val sections = Scan.repeat o section;
 
 end;
 
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -107,6 +107,11 @@
   val opt_target: (xstring * Position.T) option parser
   val args: Token.T list parser
   val args1: (string -> bool) -> Token.T list parser
+  val attribs: Token.src list parser
+  val opt_attribs: Token.src list parser
+  val thm_sel: Facts.interval list parser
+  val xthm: (Facts.ref * Token.src list) parser
+  val xthms1: (Facts.ref * Token.src list) list parser
 end;
 
 structure Parse: PARSE =
@@ -433,5 +438,27 @@
 
 end;
 
+
+(* attributes *)
+
+val attrib = position liberal_name -- !!! args >> uncurry Token.src;
+val attribs = $$$ "[" |-- list attrib --| $$$ "]";
+val opt_attribs = Scan.optional attribs [];
+
+
+(* theorem references *)
+
+val thm_sel = $$$ "(" |-- list1
+ (nat --| minus -- nat >> Facts.FromTo ||
+  nat --| minus >> Facts.From ||
+  nat >> Facts.Single) --| $$$ ")";
+
+val xthm =
+  $$$ "[" |-- attribs --| $$$ "]" >> pair (Facts.named "") ||
+  (literal_fact >> Facts.Fact ||
+    position xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
+
+val xthms1 = Scan.repeat1 xthm;
+
 end;
 
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -6,16 +6,12 @@
 
 signature PARSE_SPEC =
 sig
-  val attribs: Token.src list parser
-  val opt_attribs: Token.src list parser
   val thm_name: string -> Attrib.binding parser
   val opt_thm_name: string -> Attrib.binding parser
   val spec: (Attrib.binding * string) parser
   val specs: (Attrib.binding * string list) parser
   val alt_specs: (Attrib.binding * string) list parser
   val where_alt_specs: (Attrib.binding * string) list parser
-  val xthm: (Facts.ref * Token.src list) parser
-  val xthms1: (Facts.ref * Token.src list) list parser
   val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser
   val constdecl: (binding * string option * mixfix) parser
   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
@@ -37,14 +33,11 @@
 
 (* theorem specifications *)
 
-val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Token.src;
-val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
-val opt_attribs = Scan.optional attribs [];
-
-fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
+fun thm_name s = Parse.binding -- Parse.opt_attribs --| Parse.$$$ s;
 
 fun opt_thm_name s =
-  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
+  Scan.optional
+    ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s)
     Attrib.empty_binding;
 
 val spec = opt_thm_name ":" -- Parse.prop;
@@ -56,14 +49,7 @@
 
 val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
 
-val xthm =
-  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
-  (Parse.literal_fact >> Facts.Fact ||
-    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
-
-val xthms1 = Scan.repeat1 xthm;
-
-val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
+val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1);
 
 
 (* basic constant specifications *)
@@ -103,7 +89,7 @@
     >> Element.Assumes ||
   Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
     >> Element.Defines ||
-  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
+  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1))
     >> (curry Element.Notes "");
 
 fun plus1_unless test scan =
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -301,7 +301,7 @@
 
     val facts' = facts
       |> Attrib.partial_evaluation ctxt'
-      |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
+      |> Attrib.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
     val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res);
   in (res, lthy') end;
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Isar/token.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -66,14 +66,10 @@
   val text_of: T -> string * string
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
+  val make_value: string -> value -> T
   val get_value: T -> value option
   val map_value: (value -> value) -> T -> T
   val reports_of_value: T -> Position.report list
-  val mk_name: string -> T
-  val mk_typ: typ -> T
-  val mk_term: term -> T
-  val mk_fact: string option * thm list -> T
-  val mk_attribute: (morphism -> attribute) -> T
   val transform: morphism -> T -> T
   val transform_src: morphism -> src -> src
   val init_assignable: T -> T
@@ -380,6 +376,9 @@
 
 (* access values *)
 
+fun make_value name v =
+  Token ((name, Position.no_range), (InternalValue, name), Value (SOME v));
+
 fun get_value (Token (_, _, Value v)) = v
   | get_value _ = NONE;
 
@@ -400,17 +399,6 @@
   | _ => []);
 
 
-(* make values *)
-
-fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
-
-val mk_name = mk_value "<name>" o name0;
-val mk_typ = mk_value "<typ>" o Typ;
-val mk_term = mk_value "<term>" o Term;
-val mk_fact = mk_value "<fact>" o Fact;
-val mk_attribute = mk_value "<attribute>" o Attribute;
-
-
 (* transform *)
 
 fun transform phi =
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -41,7 +41,7 @@
 (* attribute source *)
 
 val _ = Theory.setup
-  (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse_Spec.attribs)
+  (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs)
     (fn _ => fn raw_srcs => fn ctxt =>
       let
         val i = serial ();
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -64,12 +64,6 @@
     val t' = f t;
   in if t aconv t' then NONE else SOME (t, t') end;
 
-val add_used =
-  (Thm.fold_terms o fold_types o fold_atyps)
-    (fn TFree (a, _) => insert (op =) a
-      | TVar ((a, _), _) => insert (op =) a
-      | _ => I);
-
 in
 
 fun read_termTs ctxt ss Ts =
@@ -131,8 +125,7 @@
   let
     val ctxt' = ctxt
       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
-      |> Variable.declare_thm thm
-      |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []);  (* FIXME !? *)
+      |> Variable.declare_thm thm;
     val tvars = Thm.fold_terms Term.add_tvars thm [];
     val vars = Thm.fold_terms Term.add_vars thm [];
     val insts = read_insts ctxt' mixed_insts (tvars, vars);
diff -r 62826b36ac5e -r b2b93903ab6b src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -46,7 +46,7 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
-    (Parse_Spec.xthms1 >> (fn args =>
+    (Parse.xthms1 >> (fn args =>
       Toplevel.unknown_theory o Toplevel.keep (fn state =>
         thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
 
diff -r 62826b36ac5e -r b2b93903ab6b src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -437,9 +437,9 @@
     ("define " ^ coind_prefix ^ "datatype")
     ((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
       Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
-      Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
-      Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
-      Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
+      Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
+      Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
+      Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
       >> (Toplevel.theory o mk_datatype));
 
 end;
diff -r 62826b36ac5e -r b2b93903ab6b src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -190,10 +190,10 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
-    ((@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
-     (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
-     (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
-     Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
+    ((@{keyword "elimination"} |-- Parse.!!! Parse.xthm) --
+     (@{keyword "induction"} |-- Parse.!!! Parse.xthm) --
+     (@{keyword "case_eqns"} |-- Parse.!!! Parse.xthms1) --
+     Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse.xthms1) []
      >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
 
 end;
diff -r 62826b36ac5e -r b2b93903ab6b src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Aug 22 08:43:14 2014 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Fri Aug 22 11:31:19 2014 +0200
@@ -586,10 +586,10 @@
       ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) --
   (@{keyword "intros"} |--
     Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
-  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
-  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
+  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
+  Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse.xthms1) [] --
+  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
+  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
   >> (Toplevel.theory o mk_ind);
 
 val _ =