--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 16 00:02:11 2010 +0200
@@ -337,7 +337,7 @@
|> Symbol.source {do_recover=false}
|> OuterLex.source {do_recover=SOME false} lex Position.start
|> OuterLex.source_proper
- |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
+ |> Source.source OuterLex.stopper (Parse_Spec.xthms1 >> get) NONE
|> Source.exhaust
end
--- a/src/HOL/Nominal/nominal_primrec.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun May 16 00:02:11 2010 +0200
@@ -410,7 +410,7 @@
val _ =
OuterSyntax.local_theory_to_proof "nominal_primrec"
"define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
- (options -- P.fixes -- P.for_fixes -- SpecParse.where_alt_specs
+ (options -- P.fixes -- P.for_fixes -- Parse_Spec.where_alt_specs
>> (fn ((((invs, fctxt), fixes), params), specs) =>
add_primrec_cmd invs fctxt fixes params specs));
--- a/src/HOL/Tools/Function/function_common.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Sun May 16 00:02:11 2010 +0200
@@ -355,7 +355,7 @@
>> (fn opts => fold apply_opt opts default)
in
fun function_parser default_cfg =
- config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
+ config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs
end
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun May 16 00:02:11 2010 +0200
@@ -99,7 +99,7 @@
val quotdef_parser =
Scan.optional quotdef_decl (NONE, NoSyn) --
- P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
+ P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
end
val _ =
--- a/src/HOL/Tools/choice_specification.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Sun May 16 00:02:11 2010 +0200
@@ -239,7 +239,7 @@
val specification_decl =
P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
val _ =
OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -250,7 +250,7 @@
val ax_specification_decl =
P.name --
(P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
val _ =
OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
--- a/src/HOL/Tools/inductive.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Sun May 16 00:02:11 2010 +0200
@@ -977,8 +977,8 @@
fun gen_ind_decl mk_def coind =
P.fixes -- P.for_fixes --
- Scan.optional SpecParse.where_alt_specs [] --
- Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
+ Scan.optional Parse_Spec.where_alt_specs [] --
+ Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
>> (fn (((preds, params), specs), monos) =>
(snd oo gen_add_inductive mk_def true coind preds params specs monos));
@@ -995,7 +995,7 @@
val _ =
OuterSyntax.local_theory "inductive_cases"
"create simplified instances of elimination rules (improper)" K.thy_script
- (P.and_list1 SpecParse.specs >> (snd oo inductive_cases));
+ (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
end;
--- a/src/HOL/Tools/primrec.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Sun May 16 00:02:11 2010 +0200
@@ -315,9 +315,10 @@
P.name >> pair false) --| P.$$$ ")")) (false, "");
val old_primrec_decl =
- opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
+ opt_unchecked_name --
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
-val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
+val primrec_decl = P.opt_target -- P.fixes -- Parse_Spec.where_alt_specs;
val _ =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
--- a/src/HOL/Tools/recdef.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/recdef.ML Sun May 16 00:02:11 2010 +0200
@@ -298,7 +298,7 @@
val recdef_decl =
Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+ P.name -- P.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
-- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
@@ -309,7 +309,7 @@
val defer_recdef_decl =
P.name -- Scan.repeat1 P.prop --
- Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
+ Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (Parse_Spec.xthms1 --| P.$$$ ")")) []
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
val _ =
@@ -319,7 +319,7 @@
val _ =
OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
K.thy_goal
- ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
+ ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
--- a/src/HOLCF/Tools/fixrec.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Sun May 16 00:02:11 2010 +0200
@@ -446,11 +446,11 @@
local structure P = OuterParse and K = OuterKeyword in
val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
- ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
+ ((P.opt_keyword "permissive" >> not) -- P.fixes -- Parse_Spec.where_alt_specs
>> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
- (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
+ (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
end;
--- a/src/ZF/Tools/datatype_package.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML Sun May 16 00:02:11 2010 +0200
@@ -431,9 +431,9 @@
val datatype_decl =
(Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
- Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
+ Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
>> (Toplevel.theory o mk_datatype);
val coind_prefix = if coind then "co" else "";
--- a/src/ZF/Tools/ind_cases.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML Sun May 16 00:02:11 2010 +0200
@@ -69,7 +69,7 @@
val _ =
OuterSyntax.command "inductive_cases"
"create simplified instances of elimination rules (improper)" K.thy_script
- (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
+ (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
>> (Toplevel.theory o inductive_cases));
end;
--- a/src/ZF/Tools/induct_tacs.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Sun May 16 00:02:11 2010 +0200
@@ -191,10 +191,10 @@
val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
val rep_datatype_decl =
- (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
- (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
- (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
- Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
+ (P.$$$ "elimination" |-- P.!!! Parse_Spec.xthm) --
+ (P.$$$ "induction" |-- P.!!! Parse_Spec.xthm) --
+ (P.$$$ "case_eqns" |-- P.!!! Parse_Spec.xthms1) --
+ Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! Parse_Spec.xthms1) []
>> (fn (((x, y), z), w) => rep_datatype x y z w);
val _ =
--- a/src/ZF/Tools/inductive_package.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sun May 16 00:02:11 2010 +0200
@@ -588,11 +588,11 @@
(P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
(P.$$$ "intros" |--
- P.!!! (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))) --
- Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
- Scan.optional (P.$$$ "con_defs" |-- P.!!! SpecParse.xthms1) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
+ P.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop))) --
+ Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (P.$$$ "con_defs" |-- P.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
>> (Toplevel.theory o mk_ind);
val _ = OuterSyntax.command (co_prefix ^ "inductive")
--- a/src/ZF/Tools/primrec_package.ML Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML Sun May 16 00:02:11 2010 +0200
@@ -198,7 +198,7 @@
val _ =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
- (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+ (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
>> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
end;