--- a/src/HOLCF/cont_consts.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/HOLCF/cont_consts.ML Thu Apr 26 12:00:05 2007 +0200
@@ -85,10 +85,10 @@
val transformed_decls = map transform contconst_decls;
in
thy
- |> Theory.add_consts_i normal_decls
- |> Theory.add_consts_i (map first transformed_decls)
- |> Theory.add_syntax_i (map second transformed_decls)
- |> Theory.add_trrules_i (List.concat (map third transformed_decls))
+ |> Sign.add_consts_i normal_decls
+ |> Sign.add_consts_i (map first transformed_decls)
+ |> Sign.add_syntax_i (map second transformed_decls)
+ |> Sign.add_trrules_i (List.concat (map third transformed_decls))
end;
val add_consts = gen_add_consts Sign.read_typ;
--- a/src/HOLCF/domain/syntax.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/HOLCF/domain/syntax.ML Thu Apr 26 12:00:05 2007 +0200
@@ -144,7 +144,7 @@
in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @
(if length eqs'>1 then [const_copy] else[])@
[const_bisim])
- |> Theory.add_trrules_i (List.concat(map snd ctt))
+ |> Sign.add_trrules_i (List.concat(map snd ctt))
end; (* let *)
end; (* local *)
--- a/src/Pure/Isar/constdefs.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/Isar/constdefs.ML Thu Apr 26 12:00:05 2007 +0200
@@ -49,7 +49,7 @@
val thy' =
thy
- |> Theory.add_consts_i [(c, T, mx)]
+ |> Sign.add_consts_i [(c, T, mx)]
|> PureThy.add_defs_i false [((name, def), atts)]
|-> (fn [thm] => CodegenData.add_func false thm);
in ((c, T), thy') end;
--- a/src/Pure/Isar/isar_syn.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Apr 26 12:00:05 2007 +0200
@@ -82,7 +82,7 @@
val defaultsortP =
OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
- (P.sort >> (Toplevel.theory o Theory.add_defsort));
+ (P.sort >> (Toplevel.theory o Sign.add_defsort));
val axclassP =
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
@@ -97,18 +97,18 @@
val typedeclP =
OuterSyntax.command "typedecl" "type declaration" K.thy_decl
(P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
- Toplevel.theory (Theory.add_typedecls [(a, args, mx)])));
+ Toplevel.theory (Sign.add_typedecls [(a, args, mx)])));
val typeabbrP =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
(Scan.repeat1
(P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
- >> (Toplevel.theory o Theory.add_tyabbrs o
+ >> (Toplevel.theory o Sign.add_tyabbrs o
map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
val nontermP =
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
- K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
+ K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals));
val aritiesP =
OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
@@ -123,7 +123,7 @@
val constsP =
OuterSyntax.command "consts" "declare constants" K.thy_decl
- (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
+ (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts));
val opt_overloaded = P.opt_keyword "overloaded";
@@ -139,11 +139,11 @@
val syntaxP =
OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
- (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
+ (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
val no_syntaxP =
OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
- (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax));
+ (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
(* translations *)
@@ -162,11 +162,11 @@
val translationsP =
OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
- (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
+ (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
val no_translationsP =
OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
- (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules));
+ (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
(* axioms and definitions *)
--- a/src/Pure/Isar/locale.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/Isar/locale.ML Thu Apr 26 12:00:05 2007 +0200
@@ -1551,10 +1551,10 @@
fun global_note_prefix_i kind (fully_qualified, prfx) args thy =
thy
- |> Theory.qualified_names
- |> (if fully_qualified then Theory.sticky_prefix prfx else Theory.add_path prfx)
+ |> Sign.qualified_names
+ |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
|> PureThy.note_thmss_i kind args
- ||> Theory.restore_naming thy;
+ ||> Sign.restore_naming thy;
fun local_note_prefix_i kind (fully_qualified, prfx) args ctxt =
ctxt
@@ -1726,8 +1726,8 @@
val ([pred_def], defs_thy) =
thy
|> (if bodyT <> propT then I else
- Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
- |> Theory.add_consts_i [(bname, predT, NoSyn)]
+ Sign.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
+ |> Sign.add_consts_i [(bname, predT, NoSyn)]
|> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
--- a/src/Pure/Isar/object_logic.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML Thu Apr 26 12:00:05 2007 +0200
@@ -80,8 +80,8 @@
in
-val add_judgment = gen_add_judgment Theory.add_consts;
-val add_judgment_i = gen_add_judgment Theory.add_consts_i;
+val add_judgment = gen_add_judgment Sign.add_consts;
+val add_judgment_i = gen_add_judgment Sign.add_consts_i;
end;
--- a/src/Pure/Proof/extraction.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Apr 26 12:00:05 2007 +0200
@@ -38,8 +38,8 @@
thy
|> Theory.copy
|> Theory.root_path
- |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
- |> Theory.add_consts
+ |> Sign.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
+ |> Sign.add_consts
[("typeof", "'b::{} => Type", NoSyn),
("Type", "'a::{} itself => Type", NoSyn),
("Null", "Null", NoSyn),
@@ -735,7 +735,7 @@
val fu = Type.freeze u;
val (def_thms, thy') = if t = nullt then ([], thy) else
thy
- |> Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
+ |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
|> PureThy.add_defs_i false [((extr_name s vs ^ "_def",
Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
in
@@ -752,9 +752,9 @@
in
thy
- |> Theory.absolute_path
+ |> Sign.absolute_path
|> fold_rev add_def defs
- |> Theory.restore_naming thy
+ |> Sign.restore_naming thy
end;
--- a/src/Pure/Proof/proof_syntax.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Thu Apr 26 12:00:05 2007 +0200
@@ -41,18 +41,18 @@
fun add_proof_atom_consts names thy =
thy
- |> Theory.absolute_path
- |> Theory.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
+ |> Sign.absolute_path
+ |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
(** constants for application and abstraction **)
fun add_proof_syntax thy =
thy
|> Theory.copy
- |> Theory.root_path
- |> Theory.add_defsort_i []
- |> Theory.add_types [("proof", 0, NoSyn)]
- |> Theory.add_consts_i
+ |> Sign.root_path
+ |> Sign.add_defsort_i []
+ |> Sign.add_types [("proof", 0, NoSyn)]
+ |> Sign.add_consts_i
[("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
("Abst", (aT --> proofT) --> proofT, NoSyn),
@@ -60,8 +60,8 @@
("Hyp", propT --> proofT, NoSyn),
("Oracle", propT --> proofT, NoSyn),
("MinProof", proofT, Delimfix "?")]
- |> Theory.add_nonterminals ["param", "params"]
- |> Theory.add_syntax_i
+ |> Sign.add_nonterminals ["param", "params"]
+ |> Sign.add_syntax_i
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
@@ -69,13 +69,13 @@
("", paramT --> paramT, Delimfix "'(_')"),
("", idtT --> paramsT, Delimfix "_"),
("", paramT --> paramsT, Delimfix "_")]
- |> Theory.add_modesyntax_i ("xsymbols", true)
+ |> Sign.add_modesyntax_i ("xsymbols", true)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
- |> Theory.add_modesyntax_i ("latex", false)
+ |> Sign.add_modesyntax_i ("latex", false)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
- |> Theory.add_trrules_i (map Syntax.ParsePrintRule
+ |> Sign.add_trrules_i (map Syntax.ParsePrintRule
[(Syntax.mk_appl (Constant "_Lam")
[Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
Syntax.mk_appl (Constant "_Lam")
--- a/src/Pure/ROOT.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/ROOT.ML Thu Apr 26 12:00:05 2007 +0200
@@ -101,8 +101,8 @@
structure Pure = struct val thy = theory "Pure" end;
Context.add_setup
- (Theory.del_modesyntax Syntax.default_mode Syntax.appl_syntax #>
- Theory.add_syntax Syntax.applC_syntax);
+ (Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #>
+ Sign.add_syntax Syntax.applC_syntax);
use_thy "CPure";
structure CPure = struct val thy = theory "CPure" end;
--- a/src/Pure/Thy/html.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/Thy/html.ML Thu Apr 26 12:00:05 2007 +0200
@@ -250,7 +250,7 @@
("var", style "var"),
("xstr", style "xstr")];
-val _ = Context.add_setup (Theory.add_mode_tokentrfuns htmlN html_trans);
+val _ = Context.add_setup (Sign.add_mode_tokentrfuns htmlN html_trans);
--- a/src/Pure/pure_thy.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/pure_thy.ML Thu Apr 26 12:00:05 2007 +0200
@@ -408,10 +408,10 @@
fun note_thmss_qualified k path facts thy =
thy
- |> Theory.add_path path
- |> Theory.no_base_names
+ |> Sign.add_path path
+ |> Sign.no_base_names
|> note_thmss_i k facts
- ||> Theory.restore_naming thy;
+ ||> Sign.restore_naming thy;
(* store_thm *)
@@ -487,12 +487,12 @@
val add_axioms_i = add_singles Theory.add_axioms_i;
val add_axiomss = add_multis Theory.add_axioms;
val add_axiomss_i = add_multis Theory.add_axioms_i;
- val add_defs = add_singles o (Theory.add_defs false);
- val add_defs_i = add_singles o (Theory.add_defs_i false);
- val add_defs_unchecked = add_singles o (Theory.add_defs true);
- val add_defs_unchecked_i = add_singles o (Theory.add_defs_i true);
- val add_defss = add_multis o (Theory.add_defs false);
- val add_defss_i = add_multis o (Theory.add_defs_i false);
+ val add_defs = add_singles o Theory.add_defs false;
+ val add_defs_i = add_singles o Theory.add_defs_i false;
+ val add_defs_unchecked = add_singles o Theory.add_defs true;
+ val add_defs_unchecked_i = add_singles o Theory.add_defs_i true;
+ val add_defss = add_multis o Theory.add_defs false;
+ val add_defss_i = add_multis o Theory.add_defs_i false;
end;
@@ -509,13 +509,13 @@
|> Theory.init_data
|> Proofterm.init_data
|> TheoremsData.init
- |> Theory.add_types
+ |> Sign.add_types
[("fun", 2, NoSyn),
("prop", 0, NoSyn),
("itself", 1, NoSyn),
("dummy", 0, NoSyn)]
- |> Theory.add_nonterminals Syntax.basic_nonterms
- |> Theory.add_syntax
+ |> Sign.add_nonterminals Syntax.basic_nonterms
+ |> Sign.add_syntax
[("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
("_abs", "'a", NoSyn),
("", "'a => args", Delimfix "_"),
@@ -553,8 +553,8 @@
("_struct", "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
("==>", "prop => prop => prop", Delimfix "op ==>"),
(Term.dummy_patternN, "aprop", Delimfix "'_")]
- |> Theory.add_syntax Syntax.appl_syntax
- |> Theory.add_modesyntax (Symbol.xsymbolsN, true)
+ |> Sign.add_syntax Syntax.appl_syntax
+ |> Sign.add_modesyntax (Symbol.xsymbolsN, true)
[("fun", "[type, type] => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
("_bracket", "[types, type] => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
("_ofsort", "[tid, sort] => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
@@ -569,13 +569,13 @@
("_DDDOT", "aprop", Delimfix "\\<dots>"),
("_bigimpl", "[asms, prop] => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", "logic", Delimfix "\\<dots>")]
- |> Theory.add_modesyntax ("", false)
+ |> Sign.add_modesyntax ("", false)
[("prop", "prop => prop", Mixfix ("_", [0], 0)),
("ProtoPure.term", "'a => prop", Delimfix "TERM _"),
("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
- |> Theory.add_modesyntax ("HTML", false)
+ |> Sign.add_modesyntax ("HTML", false)
[("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
- |> Theory.add_consts
+ |> Sign.add_consts
[("==", "'a => 'a => prop", InfixrName ("==", 2)),
("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
@@ -588,10 +588,10 @@
Const ("all", (aT --> propT) --> propT),
Const ("TYPE", Term.a_itselfT),
Const (Term.dummy_patternN, aT)]
- |> Theory.add_trfuns Syntax.pure_trfuns
- |> Theory.add_trfunsT Syntax.pure_trfunsT
+ |> Sign.add_trfuns Syntax.pure_trfuns
+ |> Sign.add_trfunsT Syntax.pure_trfunsT
|> Sign.local_path
- |> Theory.add_consts
+ |> Sign.add_consts
[("term", "'a => prop", NoSyn),
("conjunction", "prop => prop => prop", NoSyn)]
|> (add_defs false o map Thm.no_attributes)
--- a/src/Pure/sign.ML Thu Apr 26 12:00:01 2007 +0200
+++ b/src/Pure/sign.ML Thu Apr 26 12:00:05 2007 +0200
@@ -61,14 +61,6 @@
val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
theory -> theory
val restore_naming: theory -> theory -> theory
- val hide_classes: bool -> xstring list -> theory -> theory
- val hide_classes_i: bool -> string list -> theory -> theory
- val hide_types: bool -> xstring list -> theory -> theory
- val hide_types_i: bool -> string list -> theory -> theory
- val hide_consts: bool -> xstring list -> theory -> theory
- val hide_consts_i: bool -> string list -> theory -> theory
- val hide_names: bool -> string * xstring list -> theory -> theory
- val hide_names_i: bool -> string * string list -> theory -> theory
end
signature SIGN =
@@ -186,6 +178,14 @@
val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
include SIGN_THEORY
+ val hide_classes: bool -> xstring list -> theory -> theory
+ val hide_classes_i: bool -> string list -> theory -> theory
+ val hide_types: bool -> xstring list -> theory -> theory
+ val hide_types_i: bool -> string list -> theory -> theory
+ val hide_consts: bool -> xstring list -> theory -> theory
+ val hide_consts_i: bool -> string list -> theory -> theory
+ val hide_names: bool -> string * xstring list -> theory -> theory
+ val hide_names_i: bool -> string * string list -> theory -> theory
end
structure Sign: SIGN =