prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;
--- a/src/FOL/ex/Iff_Oracle.thy Mon May 17 15:11:25 2010 +0200
+++ b/src/FOL/ex/Iff_Oracle.thy Mon May 17 23:54:15 2010 +0200
@@ -52,7 +52,7 @@
subsection {* Oracle as proof method *}
method_setup iff = {*
- Scan.lift OuterParse.nat >> (fn n => fn ctxt =>
+ Scan.lift Parse.nat >> (fn n => fn ctxt =>
SIMPLE_METHOD
(HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
handle Fail _ => no_tac))
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon May 17 23:54:15 2010 +0200
@@ -263,31 +263,31 @@
fun scan_arg f = Args.parens f
fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n >> K true)) false
-val vc_offsets = Scan.optional (Args.bracks (OuterParse.list1
- (OuterParse.string --| Args.colon -- OuterParse.nat))) []
+val vc_offsets = Scan.optional (Args.bracks (Parse.list1
+ (Parse.string --| Args.colon -- Parse.nat))) []
val _ =
- OuterSyntax.command "boogie_open"
+ Outer_Syntax.command "boogie_open"
"Open a new Boogie environment and load a Boogie-generated .b2i file."
- OuterKeyword.thy_decl
- (scan_opt "quiet" -- OuterParse.name -- vc_offsets >>
+ Keyword.thy_decl
+ (scan_opt "quiet" -- Parse.name -- vc_offsets >>
(Toplevel.theory o boogie_open))
-val vc_name = OuterParse.name
+val vc_name = Parse.name
-val vc_label = OuterParse.name
+val vc_label = Parse.name
val vc_labels = Scan.repeat1 vc_label
val vc_paths =
- OuterParse.nat -- (Args.$$$ "-" |-- OuterParse.nat) >> (op upto) ||
- OuterParse.nat >> single
+ Parse.nat -- (Args.$$$ "-" |-- Parse.nat) >> (op upto) ||
+ Parse.nat >> single
val vc_opts =
scan_arg
(scan_val "assertion" vc_label >> VC_Single ||
scan_val "examine" vc_labels >> VC_Examine ||
- scan_val "take" ((OuterParse.list vc_paths >> flat) -- Scan.option (
+ scan_val "take" ((Parse.list vc_paths >> flat) -- Scan.option (
scan_val "without" vc_labels >> pair false ||
scan_val "and_also" vc_labels >> pair true) >> VC_Take) ||
scan_val "only" vc_labels >> VC_Only ||
@@ -295,9 +295,9 @@
Scan.succeed VC_Complete
val _ =
- OuterSyntax.command "boogie_vc"
+ Outer_Syntax.command "boogie_vc"
"Enter into proof mode for a specific verification condition."
- OuterKeyword.thy_goal
+ Keyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
@@ -305,7 +305,7 @@
val quick_timeout = 5
val default_timeout = 20
-fun timeout name = Scan.optional (scan_val name OuterParse.nat)
+fun timeout name = Scan.optional (scan_val name Parse.nat)
val status_test =
scan_arg (
@@ -328,18 +328,18 @@
f (Toplevel.theory_of state))
val _ =
- OuterSyntax.improper_command "boogie_status"
+ Outer_Syntax.improper_command "boogie_status"
"Show the name and state of all loaded verification conditions."
- OuterKeyword.diag
+ Keyword.diag
(status_test >> status_cmd ||
status_vc >> status_cmd ||
Scan.succeed (status_cmd boogie_status))
val _ =
- OuterSyntax.command "boogie_end"
+ Outer_Syntax.command "boogie_end"
"Close the current Boogie environment."
- OuterKeyword.thy_decl
+ Keyword.thy_decl
(Scan.succeed (Toplevel.theory boogie_end))
--- a/src/HOL/Decision_Procs/Approximation.thy Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon May 17 23:54:15 2010 +0200
@@ -3310,13 +3310,13 @@
by auto
method_setup approximation = {*
- Scan.lift (OuterParse.nat)
+ Scan.lift Parse.nat
--
Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
- |-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
+ |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) []
--
Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
- |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift OuterParse.nat))
+ |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat))
>>
(fn ((prec, splitting), taylor) => fn ctxt =>
SIMPLE_METHOD' (fn i =>
--- a/src/HOL/Import/import_syntax.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Import/import_syntax.ML Mon May 17 23:54:15 2010 +0200
@@ -28,25 +28,23 @@
structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
struct
-local structure P = OuterParse and K = OuterKeyword in
-
(* Parsers *)
-val import_segment = P.name >> set_import_segment
+val import_segment = Parse.name >> set_import_segment
-val import_theory = P.name >> (fn thyname =>
+val import_theory = Parse.name >> (fn thyname =>
fn thy =>
thy |> set_generating_thy thyname
|> Sign.add_path thyname
|> add_dump (";setup_theory " ^ thyname))
fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
-val skip_import_dir = P.string >> do_skip_import_dir
+val skip_import_dir = Parse.string >> do_skip_import_dir
val lower = String.map Char.toLower
fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
-val skip_import = P.short_ident >> do_skip_import
+val skip_import = Parse.short_ident >> do_skip_import
fun end_import toks =
Scan.succeed
@@ -78,7 +76,7 @@
|> add_dump ";end_setup"
end) toks
-val ignore_thms = Scan.repeat1 P.name
+val ignore_thms = Scan.repeat1 Parse.name
>> (fn ignored =>
fn thy =>
let
@@ -87,7 +85,7 @@
Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
end)
-val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn thmmaps =>
fn thy =>
let
@@ -96,7 +94,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
end)
-val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn typmaps =>
fn thy =>
let
@@ -105,7 +103,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
end)
-val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn defmaps =>
fn thy =>
let
@@ -114,7 +112,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
end)
-val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
+val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)
>> (fn renames =>
fn thy =>
let
@@ -123,7 +121,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
end)
-val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
>> (fn constmaps =>
fn thy =>
let
@@ -133,7 +131,7 @@
| (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
end)
-val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
>> (fn constmaps =>
fn thy =>
let
@@ -156,16 +154,16 @@
val get_lexes = fn () => !lexes
val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
- val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
- val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
- val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
- val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
- val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
- val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
- val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
- val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
+ val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
+ val type_mapsP = Parse.$$$ "type_maps" |-- type_maps
+ val def_mapsP = Parse.$$$ "def_maps" |-- def_maps
+ val const_mapsP = Parse.$$$ "const_maps" |-- const_maps
+ val const_movesP = Parse.$$$ "const_moves" |-- const_moves
+ val const_renamesP = Parse.$$$ "const_renames" |-- const_renames
+ val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms
+ val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps
val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
- val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
+ val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"
fun apply [] thy = thy
| apply (f::fs) thy = apply fs (f thy)
in
@@ -188,7 +186,7 @@
NONE => error "Import data already cleared - forgotten a setup_theory?"
| SOME _ => ImportData.put NONE thy
-val setup_theory = P.name
+val setup_theory = Parse.name
>>
(fn thyname =>
fn thy =>
@@ -212,64 +210,62 @@
|> Sign.parent_path
end) toks
-val set_dump = P.string -- P.string >> setup_dump
+val set_dump = Parse.string -- Parse.string >> setup_dump
fun fl_dump toks = Scan.succeed flush_dump toks
-val append_dump = (P.verbatim || P.string) >> add_dump
+val append_dump = (Parse.verbatim || Parse.string) >> add_dump
fun setup () =
- (OuterKeyword.keyword ">";
- OuterSyntax.command "import_segment"
+ (Keyword.keyword ">";
+ Outer_Syntax.command "import_segment"
"Set import segment name"
- K.thy_decl (import_segment >> Toplevel.theory);
- OuterSyntax.command "import_theory"
+ Keyword.thy_decl (import_segment >> Toplevel.theory);
+ Outer_Syntax.command "import_theory"
"Set default HOL4 theory name"
- K.thy_decl (import_theory >> Toplevel.theory);
- OuterSyntax.command "end_import"
+ Keyword.thy_decl (import_theory >> Toplevel.theory);
+ Outer_Syntax.command "end_import"
"End HOL4 import"
- K.thy_decl (end_import >> Toplevel.theory);
- OuterSyntax.command "skip_import_dir"
+ Keyword.thy_decl (end_import >> Toplevel.theory);
+ Outer_Syntax.command "skip_import_dir"
"Sets caching directory for skipping importing"
- K.thy_decl (skip_import_dir >> Toplevel.theory);
- OuterSyntax.command "skip_import"
+ Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
+ Outer_Syntax.command "skip_import"
"Switches skipping importing on or off"
- K.thy_decl (skip_import >> Toplevel.theory);
- OuterSyntax.command "setup_theory"
+ Keyword.thy_decl (skip_import >> Toplevel.theory);
+ Outer_Syntax.command "setup_theory"
"Setup HOL4 theory replaying"
- K.thy_decl (setup_theory >> Toplevel.theory);
- OuterSyntax.command "end_setup"
+ Keyword.thy_decl (setup_theory >> Toplevel.theory);
+ Outer_Syntax.command "end_setup"
"End HOL4 setup"
- K.thy_decl (end_setup >> Toplevel.theory);
- OuterSyntax.command "setup_dump"
+ Keyword.thy_decl (end_setup >> Toplevel.theory);
+ Outer_Syntax.command "setup_dump"
"Setup the dump file name"
- K.thy_decl (set_dump >> Toplevel.theory);
- OuterSyntax.command "append_dump"
+ Keyword.thy_decl (set_dump >> Toplevel.theory);
+ Outer_Syntax.command "append_dump"
"Add text to dump file"
- K.thy_decl (append_dump >> Toplevel.theory);
- OuterSyntax.command "flush_dump"
+ Keyword.thy_decl (append_dump >> Toplevel.theory);
+ Outer_Syntax.command "flush_dump"
"Write the dump to file"
- K.thy_decl (fl_dump >> Toplevel.theory);
- OuterSyntax.command "ignore_thms"
+ Keyword.thy_decl (fl_dump >> Toplevel.theory);
+ Outer_Syntax.command "ignore_thms"
"Theorems to ignore in next HOL4 theory import"
- K.thy_decl (ignore_thms >> Toplevel.theory);
- OuterSyntax.command "type_maps"
+ Keyword.thy_decl (ignore_thms >> Toplevel.theory);
+ Outer_Syntax.command "type_maps"
"Map HOL4 type names to existing Isabelle/HOL type names"
- K.thy_decl (type_maps >> Toplevel.theory);
- OuterSyntax.command "def_maps"
+ Keyword.thy_decl (type_maps >> Toplevel.theory);
+ Outer_Syntax.command "def_maps"
"Map HOL4 constant names to their primitive definitions"
- K.thy_decl (def_maps >> Toplevel.theory);
- OuterSyntax.command "thm_maps"
+ Keyword.thy_decl (def_maps >> Toplevel.theory);
+ Outer_Syntax.command "thm_maps"
"Map HOL4 theorem names to existing Isabelle/HOL theorem names"
- K.thy_decl (thm_maps >> Toplevel.theory);
- OuterSyntax.command "const_renames"
+ Keyword.thy_decl (thm_maps >> Toplevel.theory);
+ Outer_Syntax.command "const_renames"
"Rename HOL4 const names"
- K.thy_decl (const_renames >> Toplevel.theory);
- OuterSyntax.command "const_moves"
+ Keyword.thy_decl (const_renames >> Toplevel.theory);
+ Outer_Syntax.command "const_moves"
"Rename HOL4 const names to other HOL4 constants"
- K.thy_decl (const_moves >> Toplevel.theory);
- OuterSyntax.command "const_maps"
+ Keyword.thy_decl (const_moves >> Toplevel.theory);
+ Outer_Syntax.command "const_maps"
"Map HOL4 const names to existing Isabelle/HOL const names"
- K.thy_decl (const_maps >> Toplevel.theory));
+ Keyword.thy_decl (const_maps >> Toplevel.theory));
end
-
-end
--- a/src/HOL/Import/proof_kernel.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon May 17 23:54:15 2010 +0200
@@ -189,7 +189,7 @@
else Delimfix (Syntax.escape c)
fun quotename c =
- if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
+ if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
fun simple_smart_string_of_cterm ct =
let
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Mon May 17 23:54:15 2010 +0200
@@ -144,11 +144,11 @@
val setup =
Method.setup @{binding sos}
- (Scan.lift (Scan.option OuterParse.xname)
+ (Scan.lift (Scan.option Parse.xname)
>> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
"prove universal problems over the reals using sums of squares" #>
Method.setup @{binding sos_cert}
- (Scan.lift OuterParse.string
+ (Scan.lift Parse.string
>> (fn cert => fn ctxt =>
sos_solver ignore
(Sum_Of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 17 23:54:15 2010 +0200
@@ -330,7 +330,7 @@
fun thms_of_name ctxt name =
let
- val lex = OuterKeyword.get_lexicons
+ val lex = Keyword.get_lexicons
val get = maps (ProofContext.get_fact ctxt o fst)
in
Source.of_string name
--- a/src/HOL/Nominal/nominal_atoms.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon May 17 23:54:15 2010 +0200
@@ -1004,10 +1004,10 @@
(* syntax und parsing *)
-structure P = OuterParse and K = OuterKeyword;
+structure P = Parse and K = Keyword;
val _ =
- OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
- (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
+ Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
+ (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon May 17 23:54:15 2010 +0200
@@ -2076,11 +2076,10 @@
(* FIXME: The following stuff should be exported by Datatype *)
-local structure P = OuterParse and K = OuterKeyword in
-
val datatype_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
- (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
+ Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
+ Parse.type_args -- Parse.name -- Parse.opt_mixfix --
+ (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.name -- Scan.repeat Parse.typ -- Parse.opt_mixfix));
fun mk_datatype args =
let
@@ -2090,9 +2089,7 @@
in add_nominal_datatype Datatype.default_config names specs end;
val _ =
- OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
- (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
-
-end;
+ Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl
+ (Parse.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
end
--- a/src/HOL/Nominal/nominal_induct.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Mon May 17 23:54:15 2010 +0200
@@ -138,8 +138,6 @@
local
-structure P = OuterParse;
-
val avoidingN = "avoiding";
val fixingN = "arbitrary"; (* to be consistent with induct; hopefully this changes again *)
val ruleN = "rule";
@@ -165,14 +163,14 @@
Scan.repeat (unless_more_args free)) [];
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
- P.and_list' (Scan.repeat (unless_more_args free))) [];
+ Parse.and_list' (Scan.repeat (unless_more_args free))) [];
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
in
val nominal_induct_method =
- Args.mode Induct.no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) >>
(fn (no_simp, (((x, y), z), w)) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
--- a/src/HOL/Nominal/nominal_inductive.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon May 17 23:54:15 2010 +0200
@@ -672,23 +672,20 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "avoids";
+val _ = Keyword.keyword "avoids";
val _ =
- OuterSyntax.local_theory_to_proof "nominal_inductive"
- "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
- (P.xname -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
- (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
+ Outer_Syntax.local_theory_to_proof "nominal_inductive"
+ "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
+ Keyword.thy_goal
+ (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
+ (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
prove_strong_ind name avoids));
val _ =
- OuterSyntax.local_theory "equivariance"
- "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
- (P.xname -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
+ Outer_Syntax.local_theory "equivariance"
+ "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
+ (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
(fn (name, atoms) => prove_eqvt name atoms));
-end;
-
end
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon May 17 23:54:15 2010 +0200
@@ -485,17 +485,14 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.local_theory_to_proof "nominal_inductive2"
- "prove strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
- (P.xname --
- Scan.option (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) --
- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
- (P.$$$ ":" |-- P.and_list1 P.term))) []) >> (fn ((name, rule_name), avoids) =>
+ Outer_Syntax.local_theory_to_proof "nominal_inductive2"
+ "prove strong induction theorem for inductive predicate involving nominal datatypes"
+ Keyword.thy_goal
+ (Parse.xname --
+ Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.name --| Parse.$$$ ")")) --
+ (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
+ (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
prove_strong_ind name rule_name avoids));
-end;
-
end
--- a/src/HOL/Nominal/nominal_primrec.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Mon May 17 23:54:15 2010 +0200
@@ -393,28 +393,24 @@
(* outer syntax *)
-local structure P = OuterParse in
-
-val freshness_context = P.reserved "freshness_context";
-val invariant = P.reserved "invariant";
+val freshness_context = Parse.reserved "freshness_context";
+val invariant = Parse.reserved "invariant";
-fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- P.$$$ ":") scan;
+fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
-val parser1 = (freshness_context -- P.$$$ ":") |-- unless_flag P.term >> SOME;
-val parser2 = (invariant -- P.$$$ ":") |--
- (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
+val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
+val parser2 = (invariant -- Parse.$$$ ":") |--
+ (Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
(parser1 >> pair NONE);
val options =
- Scan.optional (P.$$$ "(" |-- P.!!! (parser2 --| P.$$$ ")")) (NONE, NONE);
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
val _ =
- OuterSyntax.local_theory_to_proof "nominal_primrec"
- "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
- (options -- P.fixes -- P.for_fixes -- Parse_Spec.where_alt_specs
+ Outer_Syntax.local_theory_to_proof "nominal_primrec"
+ "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
+ (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
>> (fn ((((invs, fctxt), fixes), params), specs) =>
add_primrec_cmd invs fctxt fixes params specs));
end;
-end;
-
--- a/src/HOL/Orderings.thy Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Orderings.thy Mon May 17 23:54:15 2010 +0200
@@ -422,8 +422,8 @@
(** Diagnostic command **)
val _ =
- OuterSyntax.improper_command "print_orders"
- "print order structures available to transitivity reasoner" OuterKeyword.diag
+ Outer_Syntax.improper_command "print_orders"
+ "print order structures available to transitivity reasoner" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_structures o Toplevel.context_of)));
--- a/src/HOL/Statespace/state_space.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Mon May 17 23:54:15 2010 +0200
@@ -667,37 +667,33 @@
(*** outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val type_insts =
- P.typ >> single ||
- P.$$$ "(" |-- P.!!! (P.list1 P.typ --| P.$$$ ")")
+ Parse.typ >> single ||
+ Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.typ --| Parse.$$$ ")")
-val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ);
+val comp = Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ);
fun plus1_unless test scan =
- scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
+ scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
-val mapsto = P.$$$ "=";
-val rename = P.name -- (mapsto |-- P.name);
-val renames = Scan.optional (P.$$$ "[" |-- P.!!! (P.list1 rename --| P.$$$ "]")) [];
+val mapsto = Parse.$$$ "=";
+val rename = Parse.name -- (mapsto |-- Parse.name);
+val renames = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.list1 rename --| Parse.$$$ "]")) [];
-val parent = ((type_insts -- P.xname) || (P.xname >> pair [])) -- renames
+val parent = ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
>> (fn ((insts,name),renames) => (insts,name,renames))
val statespace_decl =
- P.type_args -- P.name --
- (P.$$$ "=" |--
+ Parse.type_args -- Parse.name --
+ (Parse.$$$ "=" |--
((Scan.repeat1 comp >> pair []) ||
(plus1_unless comp parent --
- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 comp)) [])))
+ Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) [])))
val statespace_command =
- OuterSyntax.command "statespace" "define state space" K.thy_decl
+ Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
(statespace_decl >> (fn ((args,name),(parents,comps)) =>
Toplevel.theory (define_statespace args name parents comps)))
-end;
-
end;
\ No newline at end of file
--- a/src/HOL/Tools/Datatype/datatype.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon May 17 23:54:15 2010 +0200
@@ -721,8 +721,6 @@
local
-structure P = OuterParse and K = OuterKeyword
-
fun prep_datatype_decls args =
let
val names = map
@@ -732,15 +730,16 @@
in (names, specs) end;
val parse_datatype_decl =
- (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix --
- (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
+ (Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
+ Parse.type_args -- Parse.binding -- Parse.opt_mixfix --
+ (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)));
-val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
+val parse_datatype_decls = Parse.and_list1 parse_datatype_decl >> prep_datatype_decls;
in
val _ =
- OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
+ Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
(parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
end;
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon May 17 23:54:15 2010 +0200
@@ -455,18 +455,11 @@
(* outer syntax *)
-local
-
-structure P = OuterParse and K = OuterKeyword
-
-in
-
val _ =
- OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
- (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
- >> (fn (alt_names, ts) => Toplevel.print
- o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
+ Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
+ (Scan.option (Parse.$$$ "(" |-- Scan.repeat1 Parse.name --| Parse.$$$ ")") --
+ Scan.repeat1 Parse.term
+ >> (fn (alt_names, ts) =>
+ Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
end;
-
-end;
--- a/src/HOL/Tools/Function/fun.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML Mon May 17 23:54:15 2010 +0200
@@ -159,13 +159,10 @@
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
+ Outer_Syntax.local_theory "fun" "define general recursive functions (short version)"
+ Keyword.thy_decl
(function_parser fun_config
- >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config));
+ >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
end
-
-end
--- a/src/HOL/Tools/Function/function.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon May 17 23:54:15 2010 +0200
@@ -274,20 +274,19 @@
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
|> the_single |> snd
+
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
+ Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
+ Keyword.thy_goal
(function_parser default_config
>> (fn ((config, fixes), statements) => function_cmd fixes statements config))
val _ =
- OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
- (Scan.option P.term >> termination_cmd)
-
-end
+ Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
+ Keyword.thy_goal
+ (Scan.option Parse.term >> termination_cmd)
end
--- a/src/HOL/Tools/Function/function_common.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Mon May 17 23:54:15 2010 +0200
@@ -341,21 +341,19 @@
local
- structure P = OuterParse and K = OuterKeyword
-
- val option_parser = P.group "option"
- ((P.reserved "sequential" >> K Sequential)
- || ((P.reserved "default" |-- P.term) >> Default)
- || (P.reserved "domintros" >> K DomIntros)
- || (P.reserved "no_partials" >> K No_Partials)
- || (P.reserved "tailrec" >> K Tailrec))
+ val option_parser = Parse.group "option"
+ ((Parse.reserved "sequential" >> K Sequential)
+ || ((Parse.reserved "default" |-- Parse.term) >> Default)
+ || (Parse.reserved "domintros" >> K DomIntros)
+ || (Parse.reserved "no_partials" >> K No_Partials)
+ || (Parse.reserved "tailrec" >> K Tailrec))
fun config_parser default =
- (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
+ (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
>> (fn opts => fold apply_opt opts default)
in
fun function_parser default_cfg =
- config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs
+ config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
end
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon May 17 23:54:15 2010 +0200
@@ -24,8 +24,6 @@
open Nitpick_Nut
open Nitpick
-structure K = OuterKeyword and P = OuterParse
-
val auto = Unsynchronized.ref false;
val _ =
@@ -289,14 +287,14 @@
extract_params (ProofContext.init_global thy) false (default_raw_params thy)
o map (apsnd single)
-val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
val parse_value =
- Scan.repeat1 (P.minus >> single
- || Scan.repeat1 (Scan.unless P.minus P.name)
- || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
-val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+ Scan.repeat1 (Parse.minus >> single
+ || Scan.repeat1 (Scan.unless Parse.minus Parse.name)
+ || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) >> flat
+val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
val parse_params =
- Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
+ Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
fun handle_exceptions ctxt f x =
f x
@@ -375,15 +373,15 @@
|> sort_strings |> cat_lines)))))
val parse_nitpick_command =
- (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
+ (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
-val _ = OuterSyntax.improper_command "nitpick"
+val _ = Outer_Syntax.improper_command "nitpick"
"try to find a counterexample for a given subgoal using Nitpick"
- K.diag parse_nitpick_command
-val _ = OuterSyntax.command "nitpick_params"
+ Keyword.diag parse_nitpick_command
+val _ = Outer_Syntax.command "nitpick_params"
"set and display the default parameters for Nitpick"
- K.thy_decl parse_nitpick_params_command
+ Keyword.thy_decl parse_nitpick_params_command
fun auto_nitpick state =
if not (!auto) then (false, state) else pick_nits [] true 1 0 state
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon May 17 23:54:15 2010 +0200
@@ -192,8 +192,6 @@
val setup = Predicate_Compile_Core.setup
-local structure P = OuterParse
-in
(* Parser for mode annotations *)
@@ -207,15 +205,15 @@
(parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
val mode_and_opt_proposal = parse_mode_expr --
- Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE
+ Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
val opt_modes =
- Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |--
- P.enum "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE
+ Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
+ Parse.enum "," mode_and_opt_proposal --| Parse.$$$ ")" >> SOME) NONE
val opt_expected_modes =
- Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |--
- P.enum "," parse_mode_expr --| P.$$$ ")" >> SOME) NONE
+ Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
+ Parse.enum "," parse_mode_expr --| Parse.$$$ ")" >> SOME) NONE
(* Parser for options *)
@@ -224,46 +222,46 @@
val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names)
in
- Scan.optional (P.$$$ "[" |-- Scan.optional scan_compilation Pred
- -- P.enum "," scan_bool_option --| P.$$$ "]")
+ Scan.optional (Parse.$$$ "[" |-- Scan.optional scan_compilation Pred
+ -- Parse.enum "," scan_bool_option --| Parse.$$$ "]")
(Pred, [])
end
-val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_print_modes =
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
-val opt_mode = (P.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
+val opt_mode = (Parse.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
-val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
- P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
+val opt_param_modes = Scan.optional (Parse.$$$ "[" |-- Args.$$$ "mode" |-- Parse.$$$ ":" |--
+ Parse.enum ", " opt_mode --| Parse.$$$ "]" >> SOME) NONE
val stats = Scan.optional (Args.$$$ "stats" >> K true) false
val value_options =
let
- val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE
+ val expected_values = Scan.optional (Args.$$$ "expected" |-- Parse.term >> SOME) NONE
val scan_compilation =
Scan.optional
(foldl1 (op ||)
- (map (fn (s, c) => Args.$$$ s -- P.enum "," P.int >> (fn (_, ps) => (c, ps)))
+ (map (fn (s, c) => Args.$$$ s -- Parse.enum "," Parse.int >> (fn (_, ps) => (c, ps)))
compilation_names))
(Pred, [])
in
- Scan.optional (P.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| P.$$$ "]")
+ Scan.optional
+ (Parse.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| Parse.$$$ "]")
((NONE, false), (Pred, []))
end
(* code_pred command and values command *)
-val _ = OuterSyntax.local_theory_to_proof "code_pred"
+val _ = Outer_Syntax.local_theory_to_proof "code_pred"
"prove equations for predicate specified by intro/elim rules"
- OuterKeyword.thy_goal
- (opt_expected_modes -- opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+ Keyword.thy_goal
+ (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
- (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
+val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
+ (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
>> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
(Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
end
-
-end
--- a/src/HOL/Tools/Quotient/quotient_def.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon May 17 23:54:15 2010 +0200
@@ -91,20 +91,15 @@
quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
(Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
-local
- structure P = OuterParse;
-in
-
-val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
+val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
val quotdef_parser =
Scan.optional quotdef_decl (NONE, NoSyn) --
- P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
-end
+ Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
val _ =
- OuterSyntax.local_theory "quotient_definition"
+ Outer_Syntax.local_theory "quotient_definition"
"definition for constants over the quotient type"
- OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
+ Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
end; (* structure *)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Mon May 17 23:54:15 2010 +0200
@@ -91,9 +91,9 @@
val maps_attr_parser =
Args.context -- Scan.lift
- ((Args.name --| OuterParse.$$$ "=") --
- (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
- Args.name --| OuterParse.$$$ ")"))
+ ((Args.name --| Parse.$$$ "=") --
+ (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
+ Args.name --| Parse.$$$ ")"))
val _ = Context.>> (Context.map_theory
(Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
@@ -278,8 +278,8 @@
(* setup of the printing commands *)
fun improper_command (pp_fn, cmd_name, descr_str) =
- OuterSyntax.improper_command cmd_name descr_str
- OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
+ Outer_Syntax.improper_command cmd_name descr_str
+ Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
val _ = map improper_command
[(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Mon May 17 23:54:15 2010 +0200
@@ -299,16 +299,16 @@
end
val quotspec_parser =
- OuterParse.and_list1
- ((OuterParse.type_args -- OuterParse.binding) --
- OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
- (OuterParse.$$$ "/" |-- OuterParse.term))
+ Parse.and_list1
+ ((Parse.type_args -- Parse.binding) --
+ Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
+ (Parse.$$$ "/" |-- Parse.term))
-val _ = OuterKeyword.keyword "/"
+val _ = Keyword.keyword "/"
val _ =
- OuterSyntax.local_theory_to_proof "quotient_type"
+ Outer_Syntax.local_theory_to_proof "quotient_type"
"quotient type definitions (require equivalence proofs)"
- OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+ Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
end; (* structure *)
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon May 17 23:54:15 2010 +0200
@@ -311,14 +311,14 @@
val setup =
Attrib.setup (Binding.name "smt_solver")
- (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
+ (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
(Thm.declaration_attribute o K o select_solver))
"SMT solver configuration" #>
setup_timeout #>
setup_trace #>
setup_fixed_certificates #>
Attrib.setup (Binding.name "smt_certificates")
- (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
+ (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
(Thm.declaration_attribute o K o select_certificates))
"SMT certificates" #>
Method.setup (Binding.name "smt") smt_method
@@ -353,9 +353,9 @@
Pretty.big_list "Solver-specific settings:" infos])
end
-val _ = OuterSyntax.improper_command "smt_status"
- "Show the available SMT solvers and the currently selected solver."
- OuterKeyword.diag
+val _ =
+ Outer_Syntax.improper_command "smt_status"
+ "show the available SMT solvers and the currently selected solver" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
print_setup (Context.Proof (Toplevel.context_of state)))))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 17 23:54:15 2010 +0200
@@ -24,8 +24,6 @@
open ATP_Systems
open Sledgehammer_Fact_Minimizer
-structure K = OuterKeyword and P = OuterParse
-
(** Proof method used in Isar proofs **)
val neg_clausify_setup =
@@ -36,7 +34,7 @@
(** Attribute for converting a theorem into clauses **)
val parse_clausify_attribute : attribute context_parser =
- Scan.lift OuterParse.nat
+ Scan.lift Parse.nat
>> (fn i => Thm.rule_attribute (fn context => fn th =>
let val thy = Context.theory_of context in
Meson.make_meta_clause (nth (cnf_axiom thy th) i)
@@ -321,13 +319,13 @@
params |> map string_for_raw_param
|> sort_strings |> cat_lines)))))
-val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
-val parse_value = Scan.repeat1 P.xname
-val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
-val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
+val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
+val parse_value = Scan.repeat1 Parse.xname
+val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
val parse_fact_refs =
- Scan.repeat1 (Scan.unless (P.name -- Args.colon)
- (P.xname -- Scan.option Attrib.thm_sel)
+ Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
+ (Parse.xname -- Scan.option Attrib.thm_sel)
>> (fn (name, interval) =>
Facts.Named ((name, Position.none), interval)))
val parse_relevance_chunk =
@@ -340,18 +338,18 @@
>> merge_relevance_overrides))
(add_to_relevance_override [])
val parse_sledgehammer_command =
- (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
- -- Scan.option P.nat) #>> sledgehammer_trans
+ (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
+ -- Scan.option Parse.nat) #>> sledgehammer_trans
val parse_sledgehammer_params_command =
parse_params #>> sledgehammer_params_trans
val _ =
- OuterSyntax.improper_command sledgehammerN
- "search for first-order proof using automatic theorem provers" K.diag
+ Outer_Syntax.improper_command sledgehammerN
+ "search for first-order proof using automatic theorem provers" Keyword.diag
parse_sledgehammer_command
val _ =
- OuterSyntax.command sledgehammer_paramsN
- "set and display the default parameters for Sledgehammer" K.thy_decl
+ Outer_Syntax.command sledgehammer_paramsN
+ "set and display the default parameters for Sledgehammer" Keyword.thy_decl
parse_sledgehammer_params_command
val setup =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon May 17 23:54:15 2010 +0200
@@ -102,7 +102,7 @@
let val s = unyxml y in
y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
- OuterKeyword.is_keyword s) ? quote
+ Keyword.is_keyword s) ? quote
end
fun monomorphic_term subst t =
--- a/src/HOL/Tools/choice_specification.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon May 17 23:54:15 2010 +0200
@@ -232,33 +232,28 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_name = Scan.optional (P.name --| P.$$$ ":") ""
-val opt_overloaded = P.opt_keyword "overloaded";
+val opt_name = Scan.optional (Parse.name --| Parse.$$$ ":") ""
+val opt_overloaded = Parse.opt_keyword "overloaded"
val specification_decl =
- P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
+ Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
val _ =
- OuterSyntax.command "specification" "define constants by specification" K.thy_goal
+ Outer_Syntax.command "specification" "define constants by specification" Keyword.thy_goal
(specification_decl >> (fn (cos,alt_props) =>
Toplevel.print o (Toplevel.theory_to_proof
(process_spec NONE cos alt_props))))
val ax_specification_decl =
- P.name --
- (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
+ Parse.name --
+ (Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
val _ =
- OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
+ Outer_Syntax.command "ax_specification" "define constants by specification" Keyword.thy_goal
(ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
Toplevel.print o (Toplevel.theory_to_proof
(process_spec (SOME axname) cos alt_props))))
end
-
-
-end
--- a/src/HOL/Tools/inductive.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Mon May 17 23:54:15 2010 +0200
@@ -970,32 +970,28 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "monos";
+val _ = Keyword.keyword "monos";
fun gen_ind_decl mk_def coind =
- P.fixes -- P.for_fixes --
+ Parse.fixes -- Parse.for_fixes --
Scan.optional Parse_Spec.where_alt_specs [] --
- Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
+ Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
>> (fn (((preds, params), specs), monos) =>
(snd oo gen_add_inductive mk_def true coind preds params specs monos));
val ind_decl = gen_ind_decl add_ind_def;
val _ =
- OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl
+ Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
(ind_decl false);
val _ =
- OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl
+ Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
(ind_decl true);
val _ =
- OuterSyntax.local_theory "inductive_cases"
- "create simplified instances of elimination rules (improper)" K.thy_script
- (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
+ Outer_Syntax.local_theory "inductive_cases"
+ "create simplified instances of elimination rules (improper)" Keyword.thy_script
+ (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
end;
-
-end;
--- a/src/HOL/Tools/inductive_codegen.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon May 17 23:54:15 2010 +0200
@@ -775,7 +775,7 @@
add_codegen "inductive" inductive_codegen #>
Attrib.setup @{binding code_ind}
(Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
- Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+ Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add))
"introduction rules for executable predicates";
(**** Quickcheck involving inductive predicates ****)
--- a/src/HOL/Tools/inductive_set.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon May 17 23:54:15 2010 +0200
@@ -562,18 +562,14 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
val _ =
- OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl
+ Outer_Syntax.local_theory' "inductive_set" "define inductive sets" Keyword.thy_decl
(ind_set_decl false);
val _ =
- OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl
+ Outer_Syntax.local_theory' "coinductive_set" "define coinductive sets" Keyword.thy_decl
(ind_set_decl true);
end;
-
-end;
--- a/src/HOL/Tools/primrec.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Mon May 17 23:54:15 2010 +0200
@@ -307,29 +307,26 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val opt_unchecked_name =
- Scan.optional (P.$$$ "(" |-- P.!!!
- (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
- P.name >> pair false) --| P.$$$ ")")) (false, "");
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!!
+ (((Parse.$$$ "unchecked" >> K true) -- Scan.optional Parse.name "" ||
+ Parse.name >> pair false) --| Parse.$$$ ")")) (false, "");
val old_primrec_decl =
opt_unchecked_name --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop);
-val primrec_decl = P.opt_target -- P.fixes -- Parse_Spec.where_alt_specs;
+val primrec_decl = Parse.opt_target -- Parse.fixes -- Parse_Spec.where_alt_specs;
val _ =
- OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
+ Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
+ Keyword.thy_decl
((primrec_decl >> (fn ((opt_target, fixes), specs) =>
Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
|| (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
Toplevel.theory (snd o
(if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
- alt_name (map P.triple_swap eqns) o
+ alt_name (map Parse.triple_swap eqns) o
tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
end;
-
-end;
--- a/src/HOL/Tools/recdef.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/recdef.ML Mon May 17 23:54:15 2010 +0200
@@ -289,40 +289,39 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
+val _ = List.app Keyword.keyword ["permissive", "congs", "hints"];
val hints =
- P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
+ Parse.$$$ "(" |--
+ Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;
val recdef_decl =
- Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
+ Scan.optional
+ (Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "permissive" -- Parse.$$$ ")") >> K false) true --
+ Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
-- Scan.option hints
- >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
+ >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
val _ =
- OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
+ Outer_Syntax.command "recdef" "define general recursive functions (TFL)" Keyword.thy_decl
(recdef_decl >> Toplevel.theory);
val defer_recdef_decl =
- P.name -- Scan.repeat1 P.prop --
- Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (Parse_Spec.xthms1 --| P.$$$ ")")) []
+ Parse.name -- Scan.repeat1 Parse.prop --
+ Scan.optional
+ (Parse.$$$ "(" |-- Parse.$$$ "congs" |-- Parse.!!! (Parse_Spec.xthms1 --| Parse.$$$ ")")) []
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
val _ =
- OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
+ Outer_Syntax.command "defer_recdef" "defer general recursive functions (TFL)" Keyword.thy_decl
(defer_recdef_decl >> Toplevel.theory);
val _ =
- OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
- K.thy_goal
- ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
+ Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
+ Keyword.thy_goal
+ ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
+ Scan.option (Parse.$$$ "(" |-- Parse.nat --| Parse.$$$ ")")
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
end;
-
-end;
--- a/src/HOL/Tools/record.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/record.ML Mon May 17 23:54:15 2010 +0200
@@ -2460,17 +2460,14 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.command "record" "define extensible record" K.thy_decl
- (P.type_args_constrained -- P.binding --
- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
+ Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
+ (Parse.type_args_constrained -- Parse.binding --
+ (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
+ Scan.repeat1 Parse.const_binding)
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
end;
-end;
-
structure Basic_Record: BASIC_RECORD = Record;
open Basic_Record;
--- a/src/HOL/Tools/refute_isar.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/refute_isar.ML Mon May 17 23:54:15 2010 +0200
@@ -12,19 +12,16 @@
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
-val scan_parm =
- OuterParse.name
- -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
-val scan_parms = Scan.optional
- (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
+val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
+val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
(* 'refute' command *)
val _ =
- OuterSyntax.improper_command "refute"
- "try to find a model that refutes a given subgoal" OuterKeyword.diag
- (scan_parms -- Scan.optional OuterParse.nat 1 >>
+ Outer_Syntax.improper_command "refute"
+ "try to find a model that refutes a given subgoal" Keyword.diag
+ (scan_parms -- Scan.optional Parse.nat 1 >>
(fn (parms, i) =>
Toplevel.keep (fn state =>
let
@@ -36,8 +33,8 @@
(* 'refute_params' command *)
val _ =
- OuterSyntax.command "refute_params"
- "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl
+ Outer_Syntax.command "refute_params"
+ "show/store default parameters for the 'refute' command" Keyword.thy_decl
(scan_parms >> (fn parms =>
Toplevel.theory (fn thy =>
let
--- a/src/HOL/Tools/split_rule.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/split_rule.ML Mon May 17 23:54:15 2010 +0200
@@ -135,7 +135,7 @@
Attrib.setup @{binding split_format}
(Scan.lift
(Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
- OuterParse.and_list1 (Scan.repeat Args.name_source)
+ Parse.and_list1 (Scan.repeat Args.name_source)
>> (fn xss => Thm.rule_attribute (fn context =>
split_rule_goal (Context.proof_of context) xss))))
"split pair-typed subterms in premises, or function arguments" #>
--- a/src/HOL/Tools/typedef.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Mon May 17 23:54:15 2010 +0200
@@ -296,22 +296,19 @@
(** outer syntax **)
-local structure P = OuterParse in
-
-val _ = OuterKeyword.keyword "morphisms";
+val _ = Keyword.keyword "morphisms";
val _ =
- OuterSyntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
- OuterKeyword.thy_goal
- (Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
- P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
- (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
+ Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
+ Keyword.thy_goal
+ (Scan.optional (Parse.$$$ "(" |--
+ ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
+ (Parse.type_args_constrained -- Parse.binding) --
+ Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
>> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
end;
-end;
-
--- a/src/HOLCF/IOA/meta_theory/automaton.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML Mon May 17 23:54:15 2010 +0200
@@ -485,52 +485,50 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
+val _ = List.app Keyword.keyword ["signature", "actions", "inputs",
"outputs", "internals", "states", "initially", "transitions", "pre",
"post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
"rename"];
-val actionlist = P.list1 P.term;
-val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
-val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
-val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
-val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
-val initial = P.$$$ "initially" |-- P.!!! P.term;
-val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
-val pre = P.$$$ "pre" |-- P.!!! P.term;
-val post = P.$$$ "post" |-- P.!!! assign_list;
+val actionlist = Parse.list1 Parse.term;
+val inputslist = Parse.$$$ "inputs" |-- Parse.!!! actionlist;
+val outputslist = Parse.$$$ "outputs" |-- Parse.!!! actionlist;
+val internalslist = Parse.$$$ "internals" |-- Parse.!!! actionlist;
+val stateslist =
+ Parse.$$$ "states" |-- Parse.!!! (Scan.repeat1 (Parse.name --| Parse.$$$ "::" -- Parse.typ));
+val initial = Parse.$$$ "initially" |-- Parse.!!! Parse.term;
+val assign_list = Parse.list1 (Parse.name --| Parse.$$$ ":=" -- Parse.!!! Parse.term);
+val pre = Parse.$$$ "pre" |-- Parse.!!! Parse.term;
+val post = Parse.$$$ "post" |-- Parse.!!! assign_list;
val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
-val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
-val transition = P.term -- (transrel || pre1 || post1);
-val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
+val transrel = (Parse.$$$ "transrel" |-- Parse.!!! Parse.term) >> mk_trans_of_rel;
+val transition = Parse.term -- (transrel || pre1 || post1);
+val translist = Parse.$$$ "transitions" |-- Parse.!!! (Scan.repeat1 transition);
val ioa_decl =
- (P.name -- (P.$$$ "=" |--
- (P.$$$ "signature" |--
- P.!!! (P.$$$ "actions" |--
- (P.typ --
+ (Parse.name -- (Parse.$$$ "=" |--
+ (Parse.$$$ "signature" |--
+ Parse.!!! (Parse.$$$ "actions" |--
+ (Parse.typ --
(Scan.optional inputslist []) --
(Scan.optional outputslist []) --
(Scan.optional internalslist []) --
stateslist --
(Scan.optional initial "True") --
translist))))) >> mk_ioa_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
+ (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "compose" |-- Parse.!!! (Parse.list1 Parse.name))))
>> mk_composition_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
- P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
- P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
+ (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "hide_action" |--
+ Parse.!!! (Parse.list1 Parse.term -- (Parse.$$$ "in" |-- Parse.name))))) >> mk_hiding_decl ||
+ (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "restrict" |--
+ Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.list1 Parse.term))))) >> mk_restriction_decl ||
+ (Parse.name -- (Parse.$$$ "=" |--
+ (Parse.$$$ "rename" |-- (Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.term))))))
>> mk_rename_decl;
val _ =
- OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
+ Outer_Syntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" Keyword.thy_decl
(ioa_decl >> Toplevel.theory);
end;
-
-end;
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Mon May 17 23:54:15 2010 +0200
@@ -224,27 +224,25 @@
(** outer syntax **)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "lazy";
+val _ = Keyword.keyword "lazy";
val dest_decl : (bool * binding option * string) parser =
- P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
- || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+ Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
+ (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1
+ || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
>> (fn t => (true,NONE,t))
- || P.typ >> (fn t => (false,NONE,t));
+ || Parse.typ >> (fn t => (false,NONE,t));
val cons_decl =
- P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
+ Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix;
val domain_decl =
- (P.type_args_constrained -- P.binding -- P.opt_mixfix) --
- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+ (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
+ (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
val domains_decl =
- Scan.option (P.$$$ "(" |-- P.binding --| P.$$$ ")") --
- P.and_list1 domain_decl;
+ Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
+ Parse.and_list1 domain_decl;
fun mk_domain
(definitional : bool)
@@ -267,13 +265,11 @@
end;
val _ =
- OuterSyntax.command "domain" "define recursive domains (HOLCF)"
- K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
+ Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
+ Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
val _ =
- OuterSyntax.command "new_domain" "define recursive domains (HOLCF)"
- K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
+ Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
+ Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
end;
-
-end;
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon May 17 23:54:15 2010 +0200
@@ -707,21 +707,20 @@
local
-structure P = OuterParse and K = OuterKeyword
-
val parse_domain_iso :
(string list * binding * mixfix * string * (binding * binding) option)
parser =
- (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)))
+ (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
>> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs));
-val parse_domain_isos = P.and_list1 parse_domain_iso;
+val parse_domain_isos = Parse.and_list1 parse_domain_iso;
in
val _ =
- OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl
+ Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
+ Keyword.thy_decl
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd));
end;
--- a/src/HOLCF/Tools/cont_consts.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/cont_consts.ML Mon May 17 23:54:15 2010 +0200
@@ -93,12 +93,8 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
- (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd));
+ Outer_Syntax.command "consts" "declare constants (HOLCF)" Keyword.thy_decl
+ (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o add_consts_cmd));
end;
-
-end;
--- a/src/HOLCF/Tools/fixrec.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Mon May 17 23:54:15 2010 +0200
@@ -443,16 +443,14 @@
(******************************** Parsers ********************************)
(*************************************************************************)
-local structure P = OuterParse and K = OuterKeyword in
+val _ =
+ Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
+ ((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs
+ >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
-val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
- ((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
- (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
-
-end;
+val _ =
+ Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl
+ (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
val setup =
Attrib.setup @{binding fixrec_simp}
--- a/src/HOLCF/Tools/pcpodef.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Mon May 17 23:54:15 2010 +0200
@@ -355,29 +355,29 @@
(** outer syntax **)
-local structure P = OuterParse and K = OuterKeyword in
-
val typedef_proof_decl =
- Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
- --| P.$$$ ")") (true, NONE) --
- (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
+ Scan.optional (Parse.$$$ "(" |--
+ ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s)))
+ --| Parse.$$$ ")") (true, NONE) --
+ (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
+ (Parse.$$$ "=" |-- Parse.term) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
((def, the_default t opt_name), (t, args, mx), A, morphs);
val _ =
- OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+ Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
+ Keyword.thy_goal
(typedef_proof_decl >>
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
val _ =
- OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+ Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
+ Keyword.thy_goal
(typedef_proof_decl >>
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
end;
-
-end;
--- a/src/HOLCF/Tools/repdef.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML Mon May 17 23:54:15 2010 +0200
@@ -168,23 +168,21 @@
(** outer syntax **)
-local structure P = OuterParse and K = OuterKeyword in
-
val repdef_decl =
- Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
- --| P.$$$ ")") (true, NONE) --
- (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
+ Scan.optional (Parse.$$$ "(" |--
+ ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s)))
+ --| Parse.$$$ ")") (true, NONE) --
+ (Parse.type_args_constrained -- Parse.binding) --
+ Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
fun mk_repdef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
repdef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs);
val _ =
- OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl
+ Outer_Syntax.command "repdef" "HOLCF definition of representable domains" Keyword.thy_decl
(repdef_decl >>
(Toplevel.print oo (Toplevel.theory o mk_repdef)));
end;
-
-end;
--- a/src/Provers/blast.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Provers/blast.ML Mon May 17 23:54:15 2010 +0200
@@ -1309,7 +1309,7 @@
val setup =
setup_depth_limit #>
Method.setup @{binding blast}
- (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >>
+ (Scan.lift (Scan.option Parse.nat) --| Method.sections Data.cla_modifiers >>
(fn NONE => Data.cla_meth' blast_tac
| SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
"classical tableau prover";
--- a/src/Provers/clasimp.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Provers/clasimp.ML Mon May 17 23:54:15 2010 +0200
@@ -275,7 +275,7 @@
Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
val auto_method =
- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
+ Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
Method.sections clasimp_modifiers >>
(fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
| SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
--- a/src/Provers/classical.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Provers/classical.ML Mon May 17 23:54:15 2010 +0200
@@ -1015,8 +1015,8 @@
(** outer syntax **)
val _ =
- OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
- OuterKeyword.diag
+ Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
+ Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
--- a/src/Tools/Code/code_eval.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Mon May 17 23:54:15 2010 +0200
@@ -204,26 +204,24 @@
local
-structure P = OuterParse
-and K = OuterKeyword
-
val datatypesK = "datatypes";
val functionsK = "functions";
val fileK = "file";
val andK = "and"
-val _ = List.app K.keyword [datatypesK, functionsK];
+val _ = List.app Keyword.keyword [datatypesK, functionsK];
-val parse_datatype = (P.name --| P.$$$ "=" -- (P.term ::: (Scan.repeat (P.$$$ "|" |-- P.term))));
+val parse_datatype =
+ Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
in
val _ =
- OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
- K.thy_decl (P.name -- Scan.optional (P.$$$ datatypesK |-- (parse_datatype
- ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
- -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
- -- Scan.option (P.$$$ fileK |-- P.name)
+ Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
+ Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
+ ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
+ -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
+ -- Scan.option (Parse.$$$ fileK |-- Parse.name)
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
(code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
--- a/src/Tools/Code/code_haskell.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon May 17 23:54:15 2010 +0200
@@ -469,8 +469,8 @@
serialize_haskell module_prefix module_name string_classes));
val _ =
- OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
- OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
+ Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
+ Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
Toplevel.theory (add_monad target raw_bind))
);
--- a/src/Tools/Code/code_preproc.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon May 17 23:54:15 2010 +0200
@@ -479,8 +479,8 @@
end;
val _ =
- OuterSyntax.improper_command "print_codeproc" "print code preprocessor setup"
- OuterKeyword.diag (Scan.succeed
+ Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
+ Keyword.diag (Scan.succeed
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
(print_codeproc o Toplevel.theory_of)));
--- a/src/Tools/Code/code_printer.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Mon May 17 23:54:15 2010 +0200
@@ -329,15 +329,15 @@
fun parse_syntax prep_arg xs =
Scan.option ((
- ((OuterParse.$$$ infixK >> K X)
- || (OuterParse.$$$ infixlK >> K L)
- || (OuterParse.$$$ infixrK >> K R))
- -- OuterParse.nat >> parse_infix prep_arg
+ ((Parse.$$$ infixK >> K X)
+ || (Parse.$$$ infixlK >> K L)
+ || (Parse.$$$ infixrK >> K R))
+ -- Parse.nat >> parse_infix prep_arg
|| Scan.succeed (parse_mixfix prep_arg))
- -- OuterParse.string
+ -- Parse.string
>> (fn (parse, s) => parse s)) xs;
-val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
+val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
(** module name spaces **)
--- a/src/Tools/Code/code_target.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_target.ML Mon May 17 23:54:15 2010 +0200
@@ -463,9 +463,6 @@
local
-structure P = OuterParse
-and K = OuterKeyword
-
fun zip_list (x::xs) f g =
f
#-> (fn y =>
@@ -473,9 +470,9 @@
#-> (fn xys => pair ((x, y) :: xys)));
fun parse_multi_syntax parse_thing parse_syntax =
- P.and_list1 parse_thing
- #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
- (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
+ Parse.and_list1 parse_thing
+ #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
+ (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
in
@@ -507,75 +504,79 @@
val (inK, module_nameK, fileK) = ("in", "module_name", "file");
val code_exprP =
- (Scan.repeat1 P.term_group
- -- Scan.repeat (P.$$$ inK |-- P.name
- -- Scan.option (P.$$$ module_nameK |-- P.name)
- -- Scan.option (P.$$$ fileK |-- P.name)
- -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
+ (Scan.repeat1 Parse.term_group
+ -- Scan.repeat (Parse.$$$ inK |-- Parse.name
+ -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
+ -- Scan.option (Parse.$$$ fileK |-- Parse.name)
+ -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
-val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
+val _ = List.app Keyword.keyword [inK, module_nameK, fileK];
val _ =
- OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
- parse_multi_syntax P.xname (Scan.option P.string)
+ Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
+ parse_multi_syntax Parse.xname (Scan.option Parse.string)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
);
val _ =
- OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
- parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
+ Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
+ parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+ (Scan.option (Parse.minus >> K ()))
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
);
val _ =
- OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
- parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
+ Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
+ parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
);
val _ =
- OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
- parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
+ Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
+ parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
);
val _ =
- OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
- P.name -- Scan.repeat1 P.name
+ Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
+ Keyword.thy_decl (
+ Parse.name -- Scan.repeat1 Parse.name
>> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
);
val _ =
- OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
- P.name -- P.name -- (P.text :|-- (fn "-" => Scan.succeed NONE
- | s => Scan.optional (P.$$$ "attach" |-- Scan.repeat1 P.term) [] >> pair s >> SOME))
+ Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
+ Keyword.thy_decl (
+ Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
+ | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
>> (fn ((target, name), content_consts) =>
(Toplevel.theory o add_include_cmd target) (name, content_consts))
);
val _ =
- OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
- P.name -- Scan.repeat1 (P.name -- P.name)
+ Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
+ Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
>> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
);
val _ =
- OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
- Scan.repeat1 P.term_group >> (Toplevel.theory o fold allow_abort_cmd)
+ Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
+ Keyword.thy_decl (
+ Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
);
val _ =
- OuterSyntax.command "export_code" "generate executable code for constants"
- K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+ Outer_Syntax.command "export_code" "generate executable code for constants"
+ Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
fun shell_command thyname cmd = Toplevel.program (fn _ =>
- (use_thy thyname; case Scan.read Token.stopper (P.!!! code_exprP)
- ((filter Token.is_proper o OuterSyntax.scan Position.none) cmd)
+ (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
+ ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
of SOME f => (writeln "Now generating code..."; f (theory thyname))
| NONE => error ("Bad directive " ^ quote cmd)))
handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
--- a/src/Tools/Code/code_thingol.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon May 17 23:54:15 2010 +0200
@@ -915,23 +915,21 @@
local
-structure P = OuterParse
-and K = OuterKeyword
-
fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
in
val _ =
- OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
- (Scan.repeat1 P.term_group
+ Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
+ (Scan.repeat1 Parse.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
val _ =
- OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
- (Scan.repeat1 P.term_group
+ Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
+ Keyword.diag
+ (Scan.repeat1 Parse.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
--- a/src/Tools/WWW_Find/find_theorems.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Mon May 17 23:54:15 2010 +0200
@@ -158,21 +158,17 @@
end;
-structure P = OuterParse
- and K = OuterKeyword
- and FT = Find_Theorems;
-
val criterion =
- P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Find_Theorems.Name ||
- P.reserved "intro" >> K Find_Theorems.Intro ||
- P.reserved "elim" >> K Find_Theorems.Elim ||
- P.reserved "dest" >> K Find_Theorems.Dest ||
- P.reserved "solves" >> K Find_Theorems.Solves ||
- P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Find_Theorems.Simp ||
- P.term >> Find_Theorems.Pattern;
+ Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
+ Parse.reserved "intro" >> K Find_Theorems.Intro ||
+ Parse.reserved "elim" >> K Find_Theorems.Elim ||
+ Parse.reserved "dest" >> K Find_Theorems.Dest ||
+ Parse.reserved "solves" >> K Find_Theorems.Solves ||
+ Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
+ Parse.term >> Find_Theorems.Pattern;
val parse_query =
- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion));
+ Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
fun app_index f xs = fold_index (fn x => K (f x)) xs ();
@@ -194,7 +190,7 @@
fun get_query () =
query
|> (fn s => s ^ ";")
- |> OuterSyntax.scan Position.start
+ |> Outer_Syntax.scan Position.start
|> filter Token.is_proper
|> Scan.error parse_query
|> fst;
--- a/src/Tools/WWW_Find/unicode_symbols.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Mon May 17 23:54:15 2010 +0200
@@ -114,8 +114,6 @@
local (* Parser *)
-structure P = OuterParse;
-
fun $$$ kw = Scan.one (is_keyword kw) >> str_of_token;
val hex_code = Scan.one is_hex_code >> int_of_code;
val ascii_sym = Scan.one is_ascii_sym >> str_of_token;
@@ -129,7 +127,7 @@
in
-val line = (symbol -- unicode --| font -- abbr) >> P.triple1;
+val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
val symbols_path =
[getenv "ISABELLE_HOME", "etc", "symbols"]
--- a/src/Tools/eqsubst.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/eqsubst.ML Mon May 17 23:54:15 2010 +0200
@@ -556,7 +556,7 @@
(Scan.succeed false);
val ith_syntax =
- Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
+ Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
(* combination method that takes a flag (true indicates that subst
should be done to an assumption, false = apply to the conclusion of
--- a/src/Tools/induct.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/induct.ML Mon May 17 23:54:15 2010 +0200
@@ -254,8 +254,8 @@
end;
val _ =
- OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
- OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+ Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_rules o Toplevel.context_of)));
@@ -845,8 +845,6 @@
(** concrete syntax **)
-structure P = OuterParse;
-
val arbitraryN = "arbitrary";
val takingN = "taking";
val ruleN = "rule";
@@ -892,7 +890,7 @@
Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
- P.and_list1' (Scan.repeat (unless_more_args free))) [];
+ Parse.and_list1' (Scan.repeat (unless_more_args free))) [];
val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
Scan.repeat1 (unless_more_args inst)) [];
@@ -902,7 +900,7 @@
val cases_setup =
Method.setup @{binding cases}
(Args.mode no_simpN --
- (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
+ (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
(fn (no_simp, (insts, opt_rule)) => fn ctxt =>
METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
(cases_tac ctxt (not no_simp) insts opt_rule facts)))))
@@ -910,11 +908,12 @@
val induct_setup =
Method.setup @{binding induct}
- (Args.mode no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
(arbitrary -- taking -- Scan.option induct_rule)) >>
(fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
+ Seq.DETERM
+ (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
"induction on types or predicates/sets";
val coinduct_setup =
--- a/src/Tools/induct_tacs.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/induct_tacs.ML Mon May 17 23:54:15 2010 +0200
@@ -116,8 +116,7 @@
val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
val varss =
- OuterParse.and_list'
- (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
+ Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
in
--- a/src/Tools/intuitionistic.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/intuitionistic.ML Mon May 17 23:54:15 2010 +0200
@@ -71,7 +71,7 @@
val destN = "dest";
fun modifier name kind kind' att =
- Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
+ Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
>> (pair (I: Proof.context -> Proof.context) o att);
val modifiers =
@@ -87,7 +87,7 @@
fun method_setup name =
Method.setup name
- (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
+ (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
(fn opt_lim => fn ctxt =>
SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
"intuitionistic proof search";
--- a/src/Tools/nbe.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/nbe.ML Mon May 17 23:54:15 2010 +0200
@@ -625,15 +625,12 @@
val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_modes =
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
val _ =
- OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
- (opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd));
-
-end;
+ Outer_Syntax.improper_command "normal_form" "normalize term by evaluation" Keyword.diag
+ (opt_modes -- Parse.term >> (Toplevel.keep o norm_print_term_cmd));
end;
\ No newline at end of file
--- a/src/Tools/quickcheck.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/quickcheck.ML Mon May 17 23:54:15 2010 +0200
@@ -315,27 +315,25 @@
test_goal quiet report generator_name size iterations default_type no_assms insts i assms state
end;
-fun quickcheck args i state = fst (gen_quickcheck args i state)
+fun quickcheck args i state = fst (gen_quickcheck args i state);
fun quickcheck_cmd args i state =
gen_quickcheck args i (Toplevel.proof_of state)
|> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
-local structure P = OuterParse and K = OuterKeyword in
+val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true");
-val parse_arg = P.name -- (Scan.optional (P.$$$ "=" |-- P.name) "true")
-
-val parse_args = P.$$$ "[" |-- P.list1 parse_arg --| P.$$$ "]"
+val parse_args = Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]"
|| Scan.succeed [];
-val _ = OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
- (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
+val _ =
+ Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl
+ (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
-val _ = OuterSyntax.improper_command "quickcheck" "try to find counterexample for subgoal" K.diag
- (parse_args -- Scan.optional P.nat 1
- >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
-
-end; (*local*)
+val _ =
+ Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag
+ (parse_args -- Scan.optional Parse.nat 1
+ >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
end;
--- a/src/Tools/value.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/value.ML Mon May 17 23:54:15 2010 +0200
@@ -52,15 +52,13 @@
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_modes =
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
-val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
- (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
- >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
- (value_cmd some_name modes t)));
-
-end; (*local*)
+val _ =
+ Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
+ (Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]") -- opt_modes -- Parse.term
+ >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
+ (value_cmd some_name modes t)));
end;
--- a/src/ZF/Tools/datatype_package.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML Mon May 17 23:54:15 2010 +0200
@@ -419,29 +419,26 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
#1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
val con_decl =
- P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
- >> P.triple1;
+ Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] --
+ Parse.opt_mixfix >> Parse.triple1;
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.!!! Parse_Spec.xthms1) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
+ (Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") --
+ Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) --
+ Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
>> (Toplevel.theory o mk_datatype);
val coind_prefix = if coind then "co" else "";
-val _ = OuterSyntax.command (coind_prefix ^ "datatype")
- ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
+val _ =
+ Outer_Syntax.command (coind_prefix ^ "datatype")
+ ("define " ^ coind_prefix ^ "datatype") Keyword.thy_decl datatype_decl;
end;
-end;
-
--- a/src/ZF/Tools/ind_cases.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML Mon May 17 23:54:15 2010 +0200
@@ -64,15 +64,11 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.command "inductive_cases"
- "create simplified instances of elimination rules (improper)" K.thy_script
- (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
+ Outer_Syntax.command "inductive_cases"
+ "create simplified instances of elimination rules (improper)" Keyword.thy_script
+ (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
>> (Toplevel.theory o inductive_cases));
end;
-end;
-
--- a/src/ZF/Tools/induct_tacs.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon May 17 23:54:15 2010 +0200
@@ -186,25 +186,20 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
+val _ = List.app Keyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
val rep_datatype_decl =
- (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) []
+ (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
+ (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --
+ (Parse.$$$ "case_eqns" |-- Parse.!!! Parse_Spec.xthms1) --
+ Scan.optional (Parse.$$$ "recursor_eqns" |-- Parse.!!! Parse_Spec.xthms1) []
>> (fn (((x, y), z), w) => rep_datatype x y z w);
val _ =
- OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
+ Outer_Syntax.command "rep_datatype" "represent existing set inductively" Keyword.thy_decl
(rep_datatype_decl >> Toplevel.theory);
end;
-end;
-
-
val exhaust_tac = DatatypeTactics.exhaust_tac;
val induct_tac = DatatypeTactics.induct_tac;
--- a/src/ZF/Tools/inductive_package.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Mon May 17 23:54:15 2010 +0200
@@ -576,29 +576,26 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword
+val _ = List.app Keyword.keyword
["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
- #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
+ #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
val ind_decl =
- (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
- ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
- (P.$$$ "intros" |--
- 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) []
+ (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
+ ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
+ (Parse.$$$ "intros" |--
+ Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
+ Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
>> (Toplevel.theory o mk_ind);
-val _ = OuterSyntax.command (co_prefix ^ "inductive")
- ("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
+val _ =
+ Outer_Syntax.command (co_prefix ^ "inductive")
+ ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
end;
-end;
-
--- a/src/ZF/Tools/primrec_package.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML Mon May 17 23:54:15 2010 +0200
@@ -194,12 +194,11 @@
(* outer syntax *)
-structure P = OuterParse and K = OuterKeyword;
-
val _ =
- OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
- (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
- >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
+ Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
+ Keyword.thy_decl
+ (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
+ >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
end;
--- a/src/ZF/Tools/typechk.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/typechk.ML Mon May 17 23:54:15 2010 +0200
@@ -118,7 +118,7 @@
"ZF type-checking";
val _ =
- OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
+ Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_tcset o Toplevel.context_of)));