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