--- 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
--- 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)
--- 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"
--- 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))
--- 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"}
--- 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)
--- 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
--- 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));
--- 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 _ =
--- 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, [], [], []))
--- 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 **)
--- 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"
--- 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 **)
--- 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 =>
--- 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"
--- 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));
--- 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;
--- 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;
--- 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 =
--- 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;
--- 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 =
--- 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 ();
--- 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);
--- 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))));
--- 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;
--- 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;
--- 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 _ =