--- a/src/HOL/Nominal/nominal_primrec.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Jan 19 22:08:08 2007 +0100
@@ -426,7 +426,7 @@
(parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE)));
val primrec_decl =
- options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+ options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
val primrecP =
OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
--- a/src/HOL/Tools/datatype_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/datatype_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -1030,9 +1030,9 @@
val rep_datatype_decl =
Scan.option (Scan.repeat1 P.name) --
- Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
- Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
- (P.$$$ "induction" |-- P.!!! P.xthm);
+ Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
+ Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
+ (P.$$$ "induction" |-- P.!!! SpecParse.xthm);
fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
--- a/src/HOL/Tools/old_inductive_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/old_inductive_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -888,8 +888,8 @@
fun ind_decl coind =
Scan.repeat1 P.term --
(P.$$$ "intros" |--
- P.!!! (Scan.repeat (P.opt_thm_name ":" -- P.prop))) --
- Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
+ P.!!! (Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop))) --
+ Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
>> (Toplevel.theory o mk_ind coind);
val inductiveP =
@@ -900,7 +900,7 @@
val ind_cases =
- P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
+ P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
>> (Toplevel.theory o inductive_cases);
val inductive_casesP =
--- a/src/HOL/Tools/primrec_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/primrec_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -321,7 +321,7 @@
P.name >> pair false) --| P.$$$ ")")) (false, "");
val primrec_decl =
- opt_unchecked_name -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+ opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
val primrecP =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
--- a/src/HOL/Tools/recdef_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/recdef_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -314,7 +314,7 @@
val recdef_decl =
Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop) -- Scan.option hints
+ P.name -- P.term -- Scan.repeat1 (SpecParse.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);
val recdefP =
@@ -324,7 +324,7 @@
val defer_recdef_decl =
P.name -- Scan.repeat1 P.prop --
- Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
+ Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
val defer_recdefP =
@@ -333,8 +333,8 @@
val recdef_tcP =
OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
- (P.opt_locale_target --
- P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
+ (P.opt_target --
+ SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
>> (fn (((loc, thm_name), name), i) =>
Toplevel.print o Toplevel.local_theory_to_proof loc (recdef_tc thm_name name i)));
--- a/src/HOL/Tools/specification_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/specification_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -241,7 +241,7 @@
val specification_decl =
P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 (P.opt_thm_name ":" -- P.prop)
+ Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
val specificationP =
OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -252,7 +252,7 @@
val ax_specification_decl =
P.name --
(P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 (P.opt_thm_name ":" -- P.prop))
+ Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))
val ax_specificationP =
OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
--- a/src/HOLCF/fixrec_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOLCF/fixrec_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -291,7 +291,7 @@
local structure P = OuterParse and K = OuterKeyword in
-val fixrec_eqn = P.opt_thm_name ":" -- P.prop;
+val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop;
val fixrec_strict = P.opt_keyword "permissive" >> not;
@@ -304,7 +304,7 @@
(fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
(* fixpat parser *)
-val fixpat_decl = P.opt_thm_name ":" -- Scan.repeat1 P.prop;
+val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
val fixpatP =
OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
--- a/src/Pure/ProofGeneral/parsing.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/Pure/ProofGeneral/parsing.ML Fri Jan 19 22:08:08 2007 +0100
@@ -129,8 +129,8 @@
val thmnameP = (* see isar_syn.ML/theoremsP *)
let
- val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
- val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
+ val name_facts = P.and_list1 ((SpecParse.opt_thm_name "=" --| SpecParse.xthms1) >> #1)
+ val theoremsP = P.opt_target |-- name_facts >> (fn [] => "" | x::_ => x)
in
theoremsP
end
@@ -150,8 +150,8 @@
| "classes" => named_item P.name "class"
| "classrel" => named_item P.name "class"
| "consts" => named_item (P.const >> #1) "term"
- | "axioms" => named_item (P.spec_name >> (#1 o #1)) "theorem"
- | "defs" => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
+ | "axioms" => named_item (SpecParse.spec_name >> (#1 o #1)) "theorem"
+ | "defs" => named_item (opt_overloaded |-- SpecParse.spec_name >> (#1 o #1)) "theorem"
| "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
| "theorems" => named_item thmnameP "thmset"
| "lemmas" => named_item thmnameP "thmset"
@@ -164,17 +164,17 @@
fun xmls_of_thy_goal (name,toks,str) =
let
(* see isar_syn.ML/gen_theorem *)
- val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
+ val statement = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.propp);
val general_statement =
- statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
+ statement >> pair [] || Scan.repeat SpecParse.locale_element -- (P.$$$ "shows" |-- statement);
val gen_theoremP =
- P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
- Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
+ P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
+ Scan.ahead (SpecParse.locale_keyword || P.$$$ "shows")) ("", []) --
general_statement >> (fn ((locale, a), (elems, concl)) =>
fst a) (* a : (bstring * Args.src list) *)
- val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
+ val nameP = P.opt_target |-- (Scan.optional ((SpecParse.opt_thm_name ":") >> #1) "")
val thmname = nameparse "opengoal" "theorem" nameP toks
in
[D.Opengoal {thmname=SOME thmname, text=str},
--- a/src/Pure/Tools/class_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/Pure/Tools/class_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -560,7 +560,7 @@
val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
-val class_bodyP = P.!!! (Scan.repeat1 P.locale_element);
+val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
val parse_arity =
(P.xname --| P.$$$ "::" -- P.!!! P.arity)
@@ -582,7 +582,7 @@
OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
>> instance_sort_e
- || P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop)
+ || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
>> (fn (arities, defs) => instance_arity_e arities defs)
) >> (Toplevel.print oo Toplevel.theory_to_proof));
--- a/src/Pure/Tools/invoke.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/Pure/Tools/invoke.ML Fri Jan 19 22:08:08 2007 +0100
@@ -119,7 +119,7 @@
OuterSyntax.command "invoke"
"schematic invocation of locale expression in proof context"
(K.tag_proof K.prf_goal)
- (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts -- P.for_fixes
+ (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
>> (fn (((name, expr), insts), fixes) =>
Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
--- a/src/ZF/Tools/datatype_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/ZF/Tools/datatype_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -417,9 +417,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.!!! P.xthms1) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
+ Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
+ Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
+ Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
>> (Toplevel.theory o mk_datatype);
val coind_prefix = if coind then "co" else "";
--- a/src/ZF/Tools/ind_cases.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/ZF/Tools/ind_cases.ML Fri Jan 19 22:08:08 2007 +0100
@@ -82,7 +82,7 @@
local structure P = OuterParse and K = OuterKeyword in
val ind_cases =
- P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
+ P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
>> (Toplevel.theory o inductive_cases);
val inductive_casesP =
--- a/src/ZF/Tools/induct_tacs.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Fri Jan 19 22:08:08 2007 +0100
@@ -199,10 +199,10 @@
local structure P = OuterParse and K = OuterKeyword in
val rep_datatype_decl =
- (P.$$$ "elimination" |-- P.!!! P.xthm) --
- (P.$$$ "induction" |-- P.!!! P.xthm) --
- (P.$$$ "case_eqns" |-- P.!!! P.xthms1) --
- Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! P.xthms1) []
+ (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --
+ (P.$$$ "induction" |-- P.!!! SpecParse.xthm) --
+ (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) --
+ Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) []
>> (fn (((x, y), z), w) => rep_datatype x y z w);
val rep_datatypeP =
--- a/src/ZF/Tools/inductive_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/ZF/Tools/inductive_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -590,11 +590,11 @@
(P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term))) --
(P.$$$ "intros" |--
- P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
- Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
- Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
+ 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) []
>> (Toplevel.theory o mk_ind);
val inductiveP = OuterSyntax.command (co_prefix ^ "inductive")
--- a/src/ZF/Tools/primrec_package.ML Fri Jan 19 22:08:07 2007 +0100
+++ b/src/ZF/Tools/primrec_package.ML Fri Jan 19 22:08:08 2007 +0100
@@ -205,7 +205,7 @@
local structure P = OuterParse and K = OuterKeyword in
-val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
val primrecP =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl