renamed some old names Theory.xxx to Sign.xxx;
authorwenzelm
Thu Apr 26 12:00:05 2007 +0200 (2007-04-26 ago)
changeset 2279634c316d7b630
parent 22795 702542e7f88c
child 22797 4b77a43f7f58
renamed some old names Theory.xxx to Sign.xxx;
src/HOLCF/cont_consts.ML
src/HOLCF/domain/syntax.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/object_logic.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/ROOT.ML
src/Pure/Thy/html.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
     1.1 --- a/src/HOLCF/cont_consts.ML	Thu Apr 26 12:00:01 2007 +0200
     1.2 +++ b/src/HOLCF/cont_consts.ML	Thu Apr 26 12:00:05 2007 +0200
     1.3 @@ -85,10 +85,10 @@
     1.4      val transformed_decls = map transform contconst_decls;
     1.5    in
     1.6      thy
     1.7 -    |> Theory.add_consts_i normal_decls
     1.8 -    |> Theory.add_consts_i (map first transformed_decls)
     1.9 -    |> Theory.add_syntax_i (map second transformed_decls)
    1.10 -    |> Theory.add_trrules_i (List.concat (map third transformed_decls))
    1.11 +    |> Sign.add_consts_i normal_decls
    1.12 +    |> Sign.add_consts_i (map first transformed_decls)
    1.13 +    |> Sign.add_syntax_i (map second transformed_decls)
    1.14 +    |> Sign.add_trrules_i (List.concat (map third transformed_decls))
    1.15    end;
    1.16  
    1.17  val add_consts = gen_add_consts Sign.read_typ;
     2.1 --- a/src/HOLCF/domain/syntax.ML	Thu Apr 26 12:00:01 2007 +0200
     2.2 +++ b/src/HOLCF/domain/syntax.ML	Thu Apr 26 12:00:05 2007 +0200
     2.3 @@ -144,7 +144,7 @@
     2.4  in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ 
     2.5  				    (if length eqs'>1 then [const_copy] else[])@
     2.6  				    [const_bisim])
     2.7 -	 |> Theory.add_trrules_i (List.concat(map snd ctt))
     2.8 +	 |> Sign.add_trrules_i (List.concat(map snd ctt))
     2.9  end; (* let *)
    2.10  
    2.11  end; (* local *)
     3.1 --- a/src/Pure/Isar/constdefs.ML	Thu Apr 26 12:00:01 2007 +0200
     3.2 +++ b/src/Pure/Isar/constdefs.ML	Thu Apr 26 12:00:05 2007 +0200
     3.3 @@ -49,7 +49,7 @@
     3.4  
     3.5      val thy' =
     3.6        thy
     3.7 -      |> Theory.add_consts_i [(c, T, mx)]
     3.8 +      |> Sign.add_consts_i [(c, T, mx)]
     3.9        |> PureThy.add_defs_i false [((name, def), atts)]
    3.10        |-> (fn [thm] => CodegenData.add_func false thm);
    3.11    in ((c, T), thy') end;
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 26 12:00:01 2007 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 26 12:00:05 2007 +0200
     4.3 @@ -82,7 +82,7 @@
     4.4  
     4.5  val defaultsortP =
     4.6    OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     4.7 -    (P.sort >> (Toplevel.theory o Theory.add_defsort));
     4.8 +    (P.sort >> (Toplevel.theory o Sign.add_defsort));
     4.9  
    4.10  val axclassP =
    4.11    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    4.12 @@ -97,18 +97,18 @@
    4.13  val typedeclP =
    4.14    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
    4.15      (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
    4.16 -      Toplevel.theory (Theory.add_typedecls [(a, args, mx)])));
    4.17 +      Toplevel.theory (Sign.add_typedecls [(a, args, mx)])));
    4.18  
    4.19  val typeabbrP =
    4.20    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    4.21      (Scan.repeat1
    4.22        (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
    4.23 -      >> (Toplevel.theory o Theory.add_tyabbrs o
    4.24 +      >> (Toplevel.theory o Sign.add_tyabbrs o
    4.25          map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
    4.26  
    4.27  val nontermP =
    4.28    OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
    4.29 -    K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
    4.30 +    K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Sign.add_nonterminals));
    4.31  
    4.32  val aritiesP =
    4.33    OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
    4.34 @@ -123,7 +123,7 @@
    4.35  
    4.36  val constsP =
    4.37    OuterSyntax.command "consts" "declare constants" K.thy_decl
    4.38 -    (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
    4.39 +    (Scan.repeat1 P.const >> (Toplevel.theory o Sign.add_consts));
    4.40  
    4.41  val opt_overloaded = P.opt_keyword "overloaded";
    4.42  
    4.43 @@ -139,11 +139,11 @@
    4.44  
    4.45  val syntaxP =
    4.46    OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
    4.47 -    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
    4.48 +    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
    4.49  
    4.50  val no_syntaxP =
    4.51    OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
    4.52 -    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax));
    4.53 +    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
    4.54  
    4.55  
    4.56  (* translations *)
    4.57 @@ -162,11 +162,11 @@
    4.58  
    4.59  val translationsP =
    4.60    OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
    4.61 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
    4.62 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
    4.63  
    4.64  val no_translationsP =
    4.65    OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
    4.66 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules));
    4.67 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
    4.68  
    4.69  
    4.70  (* axioms and definitions *)
     5.1 --- a/src/Pure/Isar/locale.ML	Thu Apr 26 12:00:01 2007 +0200
     5.2 +++ b/src/Pure/Isar/locale.ML	Thu Apr 26 12:00:05 2007 +0200
     5.3 @@ -1551,10 +1551,10 @@
     5.4  
     5.5  fun global_note_prefix_i kind (fully_qualified, prfx) args thy =
     5.6    thy
     5.7 -  |> Theory.qualified_names
     5.8 -  |> (if fully_qualified then Theory.sticky_prefix prfx else Theory.add_path prfx)
     5.9 +  |> Sign.qualified_names
    5.10 +  |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    5.11    |> PureThy.note_thmss_i kind args
    5.12 -  ||> Theory.restore_naming thy;
    5.13 +  ||> Sign.restore_naming thy;
    5.14  
    5.15  fun local_note_prefix_i kind (fully_qualified, prfx) args ctxt =
    5.16    ctxt
    5.17 @@ -1726,8 +1726,8 @@
    5.18      val ([pred_def], defs_thy) =
    5.19        thy
    5.20        |> (if bodyT <> propT then I else
    5.21 -        Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
    5.22 -      |> Theory.add_consts_i [(bname, predT, NoSyn)]
    5.23 +        Sign.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), []))
    5.24 +      |> Sign.add_consts_i [(bname, predT, NoSyn)]
    5.25        |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])];
    5.26      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
    5.27  
     6.1 --- a/src/Pure/Isar/object_logic.ML	Thu Apr 26 12:00:01 2007 +0200
     6.2 +++ b/src/Pure/Isar/object_logic.ML	Thu Apr 26 12:00:05 2007 +0200
     6.3 @@ -80,8 +80,8 @@
     6.4  
     6.5  in
     6.6  
     6.7 -val add_judgment = gen_add_judgment Theory.add_consts;
     6.8 -val add_judgment_i = gen_add_judgment Theory.add_consts_i;
     6.9 +val add_judgment = gen_add_judgment Sign.add_consts;
    6.10 +val add_judgment_i = gen_add_judgment Sign.add_consts_i;
    6.11  
    6.12  end;
    6.13  
     7.1 --- a/src/Pure/Proof/extraction.ML	Thu Apr 26 12:00:01 2007 +0200
     7.2 +++ b/src/Pure/Proof/extraction.ML	Thu Apr 26 12:00:05 2007 +0200
     7.3 @@ -38,8 +38,8 @@
     7.4    thy
     7.5    |> Theory.copy
     7.6    |> Theory.root_path
     7.7 -  |> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
     7.8 -  |> Theory.add_consts
     7.9 +  |> Sign.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
    7.10 +  |> Sign.add_consts
    7.11        [("typeof", "'b::{} => Type", NoSyn),
    7.12         ("Type", "'a::{} itself => Type", NoSyn),
    7.13         ("Null", "Null", NoSyn),
    7.14 @@ -735,7 +735,7 @@
    7.15               val fu = Type.freeze u;
    7.16               val (def_thms, thy') = if t = nullt then ([], thy) else
    7.17                 thy
    7.18 -               |> Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
    7.19 +               |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
    7.20                 |> PureThy.add_defs_i false [((extr_name s vs ^ "_def",
    7.21                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
    7.22             in
    7.23 @@ -752,9 +752,9 @@
    7.24  
    7.25    in
    7.26      thy
    7.27 -    |> Theory.absolute_path
    7.28 +    |> Sign.absolute_path
    7.29      |> fold_rev add_def defs
    7.30 -    |> Theory.restore_naming thy
    7.31 +    |> Sign.restore_naming thy
    7.32    end;
    7.33  
    7.34  
     8.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Apr 26 12:00:01 2007 +0200
     8.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu Apr 26 12:00:05 2007 +0200
     8.3 @@ -41,18 +41,18 @@
     8.4  
     8.5  fun add_proof_atom_consts names thy =
     8.6    thy
     8.7 -  |> Theory.absolute_path
     8.8 -  |> Theory.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
     8.9 +  |> Sign.absolute_path
    8.10 +  |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
    8.11  
    8.12  (** constants for application and abstraction **)
    8.13  
    8.14  fun add_proof_syntax thy =
    8.15    thy
    8.16    |> Theory.copy
    8.17 -  |> Theory.root_path
    8.18 -  |> Theory.add_defsort_i []
    8.19 -  |> Theory.add_types [("proof", 0, NoSyn)]
    8.20 -  |> Theory.add_consts_i
    8.21 +  |> Sign.root_path
    8.22 +  |> Sign.add_defsort_i []
    8.23 +  |> Sign.add_types [("proof", 0, NoSyn)]
    8.24 +  |> Sign.add_consts_i
    8.25        [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    8.26         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    8.27         ("Abst", (aT --> proofT) --> proofT, NoSyn),
    8.28 @@ -60,8 +60,8 @@
    8.29         ("Hyp", propT --> proofT, NoSyn),
    8.30         ("Oracle", propT --> proofT, NoSyn),
    8.31         ("MinProof", proofT, Delimfix "?")]
    8.32 -  |> Theory.add_nonterminals ["param", "params"]
    8.33 -  |> Theory.add_syntax_i
    8.34 +  |> Sign.add_nonterminals ["param", "params"]
    8.35 +  |> Sign.add_syntax_i
    8.36        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    8.37         ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    8.38         ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    8.39 @@ -69,13 +69,13 @@
    8.40         ("", paramT --> paramT, Delimfix "'(_')"),
    8.41         ("", idtT --> paramsT, Delimfix "_"),
    8.42         ("", paramT --> paramsT, Delimfix "_")]
    8.43 -  |> Theory.add_modesyntax_i ("xsymbols", true)
    8.44 +  |> Sign.add_modesyntax_i ("xsymbols", true)
    8.45        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
    8.46         ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    8.47         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
    8.48 -  |> Theory.add_modesyntax_i ("latex", false)
    8.49 +  |> Sign.add_modesyntax_i ("latex", false)
    8.50        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
    8.51 -  |> Theory.add_trrules_i (map Syntax.ParsePrintRule
    8.52 +  |> Sign.add_trrules_i (map Syntax.ParsePrintRule
    8.53        [(Syntax.mk_appl (Constant "_Lam")
    8.54            [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    8.55          Syntax.mk_appl (Constant "_Lam")
     9.1 --- a/src/Pure/ROOT.ML	Thu Apr 26 12:00:01 2007 +0200
     9.2 +++ b/src/Pure/ROOT.ML	Thu Apr 26 12:00:05 2007 +0200
     9.3 @@ -101,8 +101,8 @@
     9.4  structure Pure = struct val thy = theory "Pure" end;
     9.5  
     9.6  Context.add_setup
     9.7 - (Theory.del_modesyntax Syntax.default_mode Syntax.appl_syntax #>
     9.8 -  Theory.add_syntax Syntax.applC_syntax);
     9.9 + (Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #>
    9.10 +  Sign.add_syntax Syntax.applC_syntax);
    9.11  use_thy "CPure";
    9.12  structure CPure = struct val thy = theory "CPure" end;
    9.13  
    10.1 --- a/src/Pure/Thy/html.ML	Thu Apr 26 12:00:01 2007 +0200
    10.2 +++ b/src/Pure/Thy/html.ML	Thu Apr 26 12:00:05 2007 +0200
    10.3 @@ -250,7 +250,7 @@
    10.4    ("var",   style "var"),
    10.5    ("xstr",  style "xstr")];
    10.6  
    10.7 -val _ = Context.add_setup (Theory.add_mode_tokentrfuns htmlN html_trans);
    10.8 +val _ = Context.add_setup (Sign.add_mode_tokentrfuns htmlN html_trans);
    10.9  
   10.10  
   10.11  
    11.1 --- a/src/Pure/pure_thy.ML	Thu Apr 26 12:00:01 2007 +0200
    11.2 +++ b/src/Pure/pure_thy.ML	Thu Apr 26 12:00:05 2007 +0200
    11.3 @@ -408,10 +408,10 @@
    11.4  
    11.5  fun note_thmss_qualified k path facts thy =
    11.6    thy
    11.7 -  |> Theory.add_path path
    11.8 -  |> Theory.no_base_names
    11.9 +  |> Sign.add_path path
   11.10 +  |> Sign.no_base_names
   11.11    |> note_thmss_i k facts
   11.12 -  ||> Theory.restore_naming thy;
   11.13 +  ||> Sign.restore_naming thy;
   11.14  
   11.15  
   11.16  (* store_thm *)
   11.17 @@ -487,12 +487,12 @@
   11.18    val add_axioms_i         = add_singles Theory.add_axioms_i;
   11.19    val add_axiomss          = add_multis Theory.add_axioms;
   11.20    val add_axiomss_i        = add_multis Theory.add_axioms_i;
   11.21 -  val add_defs             = add_singles o (Theory.add_defs false);
   11.22 -  val add_defs_i           = add_singles o (Theory.add_defs_i false);
   11.23 -  val add_defs_unchecked   = add_singles o (Theory.add_defs true);
   11.24 -  val add_defs_unchecked_i = add_singles o (Theory.add_defs_i true);
   11.25 -  val add_defss            = add_multis o (Theory.add_defs false);
   11.26 -  val add_defss_i          = add_multis o (Theory.add_defs_i false);
   11.27 +  val add_defs             = add_singles o Theory.add_defs false;
   11.28 +  val add_defs_i           = add_singles o Theory.add_defs_i false;
   11.29 +  val add_defs_unchecked   = add_singles o Theory.add_defs true;
   11.30 +  val add_defs_unchecked_i = add_singles o Theory.add_defs_i true;
   11.31 +  val add_defss            = add_multis o Theory.add_defs false;
   11.32 +  val add_defss_i          = add_multis o Theory.add_defs_i false;
   11.33  end;
   11.34  
   11.35  
   11.36 @@ -509,13 +509,13 @@
   11.37    |> Theory.init_data
   11.38    |> Proofterm.init_data
   11.39    |> TheoremsData.init
   11.40 -  |> Theory.add_types
   11.41 +  |> Sign.add_types
   11.42     [("fun", 2, NoSyn),
   11.43      ("prop", 0, NoSyn),
   11.44      ("itself", 1, NoSyn),
   11.45      ("dummy", 0, NoSyn)]
   11.46 -  |> Theory.add_nonterminals Syntax.basic_nonterms
   11.47 -  |> Theory.add_syntax
   11.48 +  |> Sign.add_nonterminals Syntax.basic_nonterms
   11.49 +  |> Sign.add_syntax
   11.50     [("_lambda",     "[pttrns, 'a] => logic",     Mixfix ("(3%_./ _)", [0, 3], 3)),
   11.51      ("_abs",        "'a",                        NoSyn),
   11.52      ("",            "'a => args",                Delimfix "_"),
   11.53 @@ -553,8 +553,8 @@
   11.54      ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000)),
   11.55      ("==>",         "prop => prop => prop",      Delimfix "op ==>"),
   11.56      (Term.dummy_patternN, "aprop",               Delimfix "'_")]
   11.57 -  |> Theory.add_syntax Syntax.appl_syntax
   11.58 -  |> Theory.add_modesyntax (Symbol.xsymbolsN, true)
   11.59 +  |> Sign.add_syntax Syntax.appl_syntax
   11.60 +  |> Sign.add_modesyntax (Symbol.xsymbolsN, true)
   11.61     [("fun",      "[type, type] => type",  Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   11.62      ("_bracket", "[types, type] => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
   11.63      ("_ofsort",  "[tid, sort] => type",   Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
   11.64 @@ -569,13 +569,13 @@
   11.65      ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
   11.66      ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   11.67      ("_DDDOT",   "logic",                 Delimfix "\\<dots>")]
   11.68 -  |> Theory.add_modesyntax ("", false)
   11.69 +  |> Sign.add_modesyntax ("", false)
   11.70     [("prop", "prop => prop", Mixfix ("_", [0], 0)),
   11.71      ("ProtoPure.term", "'a => prop", Delimfix "TERM _"),
   11.72      ("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
   11.73 -  |> Theory.add_modesyntax ("HTML", false)
   11.74 +  |> Sign.add_modesyntax ("HTML", false)
   11.75     [("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   11.76 -  |> Theory.add_consts
   11.77 +  |> Sign.add_consts
   11.78     [("==", "'a => 'a => prop", InfixrName ("==", 2)),
   11.79      ("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   11.80      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   11.81 @@ -588,10 +588,10 @@
   11.82       Const ("all", (aT --> propT) --> propT),
   11.83       Const ("TYPE", Term.a_itselfT),
   11.84       Const (Term.dummy_patternN, aT)]
   11.85 -  |> Theory.add_trfuns Syntax.pure_trfuns
   11.86 -  |> Theory.add_trfunsT Syntax.pure_trfunsT
   11.87 +  |> Sign.add_trfuns Syntax.pure_trfuns
   11.88 +  |> Sign.add_trfunsT Syntax.pure_trfunsT
   11.89    |> Sign.local_path
   11.90 -  |> Theory.add_consts
   11.91 +  |> Sign.add_consts
   11.92     [("term", "'a => prop", NoSyn),
   11.93      ("conjunction", "prop => prop => prop", NoSyn)]
   11.94    |> (add_defs false o map Thm.no_attributes)
    12.1 --- a/src/Pure/sign.ML	Thu Apr 26 12:00:01 2007 +0200
    12.2 +++ b/src/Pure/sign.ML	Thu Apr 26 12:00:05 2007 +0200
    12.3 @@ -61,14 +61,6 @@
    12.4    val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    12.5      theory -> theory
    12.6    val restore_naming: theory -> theory -> theory
    12.7 -  val hide_classes: bool -> xstring list -> theory -> theory
    12.8 -  val hide_classes_i: bool -> string list -> theory -> theory
    12.9 -  val hide_types: bool -> xstring list -> theory -> theory
   12.10 -  val hide_types_i: bool -> string list -> theory -> theory
   12.11 -  val hide_consts: bool -> xstring list -> theory -> theory
   12.12 -  val hide_consts_i: bool -> string list -> theory -> theory
   12.13 -  val hide_names: bool -> string * xstring list -> theory -> theory
   12.14 -  val hide_names_i: bool -> string * string list -> theory -> theory
   12.15  end
   12.16  
   12.17  signature SIGN =
   12.18 @@ -186,6 +178,14 @@
   12.19    val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
   12.20    val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
   12.21    include SIGN_THEORY
   12.22 +  val hide_classes: bool -> xstring list -> theory -> theory
   12.23 +  val hide_classes_i: bool -> string list -> theory -> theory
   12.24 +  val hide_types: bool -> xstring list -> theory -> theory
   12.25 +  val hide_types_i: bool -> string list -> theory -> theory
   12.26 +  val hide_consts: bool -> xstring list -> theory -> theory
   12.27 +  val hide_consts_i: bool -> string list -> theory -> theory
   12.28 +  val hide_names: bool -> string * xstring list -> theory -> theory
   12.29 +  val hide_names_i: bool -> string * string list -> theory -> theory
   12.30  end
   12.31  
   12.32  structure Sign: SIGN =