# HG changeset patch
# User wenzelm
# Date 1408654119 -7200
# Node ID e4250d3706575e0f4b183e37d61e1be03ec45996
# Parent  dc58ab4d9f441ad492534a2de03382f2651263c7
tuned signature -- define some elementary operations earlier;

diff -r dc58ab4d9f44 -r e4250d370657 src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/recdef.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 21 22:48:39 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
@@ -232,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;
@@ -257,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;
@@ -278,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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/calculation.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/element.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Aug 21 22:48:39 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 dc58ab4d9f44 -r e4250d370657 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Aug 21 22:48:39 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 _ =