replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
authorwenzelm
Fri Apr 16 21:28:09 2010 +0200 (2010-04-16)
changeset 361763fe7e97ccca8
parent 36175 5cec4ca719d1
child 36177 8e0770d2e499
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
doc-src/Codegen/Thy/Program.thy
doc-src/Locales/Locales/Examples.thy
doc-src/Locales/Locales/document/Examples.tex
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Documents/Documents.thy
doc-src/TutorialI/Misc/Option2.thy
doc-src/TutorialI/Types/Overloading.thy
src/FOL/FOL.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Code_Evaluation.thy
src/HOL/Code_Numeral.thy
src/HOL/DSequence.thy
src/HOL/Datatype.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Groups.thy
src/HOL/HOL.thy
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Int.thy
src/HOL/Lattice/Bounds.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Fset.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/Transitive_Closure_Table.thy
src/HOL/List.thy
src/HOL/NSA/Filter.thy
src/HOL/Nat.thy
src/HOL/New_DSequence.thy
src/HOL/New_Random_Sequence.thy
src/HOL/Nitpick.thy
src/HOL/Option.thy
src/HOL/Predicate.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
src/HOL/Product_Type.thy
src/HOL/Quickcheck.thy
src/HOL/Random.thy
src/HOL/Random_Sequence.thy
src/HOL/Record.thy
src/HOL/String.thy
src/HOL/Sum_Type.thy
src/HOL/Typerep.thy
src/HOL/Word/BinGeneral.thy
src/HOL/ex/Meson_Test.thy
src/HOL/ex/Numeral.thy
src/HOL/ex/RPred.thy
src/HOL/ex/SVC_Oracle.thy
src/HOLCF/Fixrec.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/Universal.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/doc-src/Codegen/Thy/Program.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Program.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -430,7 +430,7 @@
     1.4  
     1.5  subsection {* Inductive Predicates *}
     1.6  (*<*)
     1.7 -hide const append
     1.8 +hide_const append
     1.9  
    1.10  inductive append
    1.11  where
     2.1 --- a/doc-src/Locales/Locales/Examples.thy	Fri Apr 16 20:56:40 2010 +0200
     2.2 +++ b/doc-src/Locales/Locales/Examples.thy	Fri Apr 16 21:28:09 2010 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -hide %invisible const Lattices.lattice
     2.8 +hide_const %invisible Lattices.lattice
     2.9  pretty_setmargin %invisible 65
    2.10  
    2.11  (*
     3.1 --- a/doc-src/Locales/Locales/document/Examples.tex	Fri Apr 16 20:56:40 2010 +0200
     3.2 +++ b/doc-src/Locales/Locales/document/Examples.tex	Fri Apr 16 21:28:09 2010 +0200
     3.3 @@ -25,8 +25,8 @@
     3.4  \endisadeliminvisible
     3.5  %
     3.6  \isataginvisible
     3.7 -\isacommand{hide}\isamarkupfalse%
     3.8 -\ const\ Lattices{\isachardot}lattice\isanewline
     3.9 +\isacommand{hide{\isacharunderscore}const}\isamarkupfalse%
    3.10 +\ Lattices{\isachardot}lattice\isanewline
    3.11  \isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse%
    3.12  \ {\isadigit{6}}{\isadigit{5}}%
    3.13  \endisataginvisible
     4.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Fri Apr 16 20:56:40 2010 +0200
     4.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Fri Apr 16 21:28:09 2010 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  Consider the following model of terms
     4.5  where function symbols can be applied to a list of arguments:
     4.6  *}
     4.7 -(*<*)hide const Var(*>*)
     4.8 +(*<*)hide_const Var(*>*)
     4.9  datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
    4.10  
    4.11  text{*\noindent
     5.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Fri Apr 16 20:56:40 2010 +0200
     5.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Fri Apr 16 21:28:09 2010 +0200
     5.3 @@ -138,7 +138,7 @@
     5.4  *}
     5.5  
     5.6  (*<*)
     5.7 -hide const xor
     5.8 +hide_const xor
     5.9  setup {* Sign.add_path "version1" *}
    5.10  (*>*)
    5.11  definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
    5.12 @@ -161,7 +161,7 @@
    5.13  *}
    5.14  
    5.15  (*<*)
    5.16 -hide const xor
    5.17 +hide_const xor
    5.18  setup {* Sign.add_path "version2" *}
    5.19  (*>*)
    5.20  definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
     6.1 --- a/doc-src/TutorialI/Misc/Option2.thy	Fri Apr 16 20:56:40 2010 +0200
     6.2 +++ b/doc-src/TutorialI/Misc/Option2.thy	Fri Apr 16 21:28:09 2010 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  (*<*)
     6.5  theory Option2 imports Main begin
     6.6 -hide const None Some
     6.7 -hide type option
     6.8 +hide_const None Some
     6.9 +hide_type option
    6.10  (*>*)
    6.11  
    6.12  text{*\indexbold{*option (type)}\indexbold{*None (constant)}%
     7.1 --- a/doc-src/TutorialI/Types/Overloading.thy	Fri Apr 16 20:56:40 2010 +0200
     7.2 +++ b/doc-src/TutorialI/Types/Overloading.thy	Fri Apr 16 21:28:09 2010 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  (*<*)theory Overloading imports Main Setup begin
     7.5  
     7.6 -hide (open) "class" plus (*>*)
     7.7 +hide_class (open) plus (*>*)
     7.8  
     7.9  text {* Type classes allow \emph{overloading}; thus a constant may
    7.10  have multiple definitions at non-overlapping types. *}
     8.1 --- a/src/FOL/FOL.thy	Fri Apr 16 20:56:40 2010 +0200
     8.2 +++ b/src/FOL/FOL.thy	Fri Apr 16 21:28:09 2010 +0200
     8.3 @@ -371,7 +371,7 @@
     8.4  lemmas induct_rulify_fallback =
     8.5    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     8.6  
     8.7 -hide const induct_forall induct_implies induct_equal induct_conj
     8.8 +hide_const induct_forall induct_implies induct_equal induct_conj
     8.9  
    8.10  
    8.11  text {* Method setup. *}
     9.1 --- a/src/HOL/Bali/Basis.thy	Fri Apr 16 20:56:40 2010 +0200
     9.2 +++ b/src/HOL/Bali/Basis.thy	Fri Apr 16 21:28:09 2010 +0200
     9.3 @@ -176,7 +176,7 @@
     9.4  
     9.5  section "sums"
     9.6  
     9.7 -hide const In0 In1
     9.8 +hide_const In0 In1
     9.9  
    9.10  notation sum_case  (infixr "'(+')"80)
    9.11  
    10.1 --- a/src/HOL/Bali/TypeSafe.thy	Fri Apr 16 20:56:40 2010 +0200
    10.2 +++ b/src/HOL/Bali/TypeSafe.thy	Fri Apr 16 21:28:09 2010 +0200
    10.3 @@ -9,7 +9,7 @@
    10.4  
    10.5  section "error free"
    10.6   
    10.7 -hide const field
    10.8 +hide_const field
    10.9  
   10.10  lemma error_free_halloc:
   10.11    assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
    11.1 --- a/src/HOL/Code_Evaluation.thy	Fri Apr 16 20:56:40 2010 +0200
    11.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Apr 16 21:28:09 2010 +0200
    11.3 @@ -280,8 +280,8 @@
    11.4  end
    11.5  *}
    11.6  
    11.7 -hide const dummy_term App valapp
    11.8 -hide (open) const Const termify valtermify term_of term_of_num
    11.9 +hide_const dummy_term App valapp
   11.10 +hide_const (open) Const termify valtermify term_of term_of_num
   11.11  
   11.12  subsection {* Tracing of generated and evaluated code *}
   11.13  
   11.14 @@ -301,7 +301,7 @@
   11.15  code_const "tracing :: String.literal => 'a => 'a"
   11.16    (Eval "Code'_Evaluation.tracing")
   11.17  
   11.18 -hide (open) const tracing
   11.19 +hide_const (open) tracing
   11.20  code_reserved Eval Code_Evaluation
   11.21  
   11.22  subsection {* Evaluation setup *}
    12.1 --- a/src/HOL/Code_Numeral.thy	Fri Apr 16 20:56:40 2010 +0200
    12.2 +++ b/src/HOL/Code_Numeral.thy	Fri Apr 16 21:28:09 2010 +0200
    12.3 @@ -278,7 +278,7 @@
    12.4    then show ?thesis by (auto simp add: int_of_def mult_ac)
    12.5  qed
    12.6  
    12.7 -hide (open) const of_nat nat_of int_of
    12.8 +hide_const (open) of_nat nat_of int_of
    12.9  
   12.10  subsubsection {* Lazy Evaluation of an indexed function *}
   12.11  
   12.12 @@ -289,7 +289,7 @@
   12.13  
   12.14  termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
   12.15  
   12.16 -hide (open) const iterate_upto
   12.17 +hide_const (open) iterate_upto
   12.18  
   12.19  subsection {* Code generator setup *}
   12.20  
    13.1 --- a/src/HOL/DSequence.thy	Fri Apr 16 20:56:40 2010 +0200
    13.2 +++ b/src/HOL/DSequence.thy	Fri Apr 16 21:28:09 2010 +0200
    13.3 @@ -97,13 +97,13 @@
    13.4  
    13.5  code_reserved Eval DSequence
    13.6  (*
    13.7 -hide type Sequence.seq
    13.8 +hide_type Sequence.seq
    13.9  
   13.10 -hide const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
   13.11 +hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
   13.12    Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
   13.13  *)
   13.14 -hide (open) const empty single eval map_seq bind union if_seq not_seq map
   13.15 -hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def
   13.16 +hide_const (open) empty single eval map_seq bind union if_seq not_seq map
   13.17 +hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def
   13.18    if_seq_def not_seq_def map_def
   13.19  
   13.20  end
    14.1 --- a/src/HOL/Datatype.thy	Fri Apr 16 20:56:40 2010 +0200
    14.2 +++ b/src/HOL/Datatype.thy	Fri Apr 16 21:28:09 2010 +0200
    14.3 @@ -512,8 +512,8 @@
    14.4  
    14.5  
    14.6  text {* hides popular names *}
    14.7 -hide (open) type node item
    14.8 -hide (open) const Push Node Atom Leaf Numb Lim Split Case
    14.9 +hide_type (open) node item
   14.10 +hide_const (open) Push Node Atom Leaf Numb Lim Split Case
   14.11  
   14.12  use "Tools/Datatype/datatype.ML"
   14.13  
    15.1 --- a/src/HOL/Finite_Set.thy	Fri Apr 16 20:56:40 2010 +0200
    15.2 +++ b/src/HOL/Finite_Set.thy	Fri Apr 16 21:28:09 2010 +0200
    15.3 @@ -513,7 +513,7 @@
    15.4  class finite =
    15.5    assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
    15.6  setup {* Sign.parent_path *}
    15.7 -hide const finite
    15.8 +hide_const finite
    15.9  
   15.10  context finite
   15.11  begin
    16.1 --- a/src/HOL/Fun.thy	Fri Apr 16 20:56:40 2010 +0200
    16.2 +++ b/src/HOL/Fun.thy	Fri Apr 16 21:28:09 2010 +0200
    16.3 @@ -525,7 +525,7 @@
    16.4  lemma bij_swap_iff: "bij (swap a b f) = bij f"
    16.5  by (simp add: bij_def)
    16.6  
    16.7 -hide (open) const swap
    16.8 +hide_const (open) swap
    16.9  
   16.10  
   16.11  subsection {* Inversion of injective functions *}
    17.1 --- a/src/HOL/Groups.thy	Fri Apr 16 20:56:40 2010 +0200
    17.2 +++ b/src/HOL/Groups.thy	Fri Apr 16 21:28:09 2010 +0200
    17.3 @@ -88,7 +88,7 @@
    17.4  class one =
    17.5    fixes one  :: 'a  ("1")
    17.6  
    17.7 -hide (open) const zero one
    17.8 +hide_const (open) zero one
    17.9  
   17.10  syntax
   17.11    "_index1"  :: index    ("\<^sub>1")
    18.1 --- a/src/HOL/HOL.thy	Fri Apr 16 20:56:40 2010 +0200
    18.2 +++ b/src/HOL/HOL.thy	Fri Apr 16 21:28:09 2010 +0200
    18.3 @@ -1567,7 +1567,7 @@
    18.4  lemma [induct_simp]: "(x = x) = True" 
    18.5    by (rule simp_thms)
    18.6  
    18.7 -hide const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
    18.8 +hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
    18.9  
   18.10  use "~~/src/Tools/induct_tacs.ML"
   18.11  setup InductTacs.setup
   18.12 @@ -1886,8 +1886,8 @@
   18.13    Nbe.add_const_alias @{thm equals_alias_cert}
   18.14  *}
   18.15  
   18.16 -hide (open) const eq
   18.17 -hide const eq
   18.18 +hide_const (open) eq
   18.19 +hide_const eq
   18.20  
   18.21  text {* Cases *}
   18.22  
    19.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Apr 16 20:56:40 2010 +0200
    19.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Apr 16 21:28:09 2010 +0200
    19.3 @@ -92,7 +92,7 @@
    19.4       return a
    19.5     done)"
    19.6  
    19.7 -hide (open) const new map -- {* avoid clashed with some popular names *}
    19.8 +hide_const (open) new map -- {* avoid clashed with some popular names *}
    19.9  
   19.10  
   19.11  subsection {* Properties *}
   19.12 @@ -115,28 +115,28 @@
   19.13  
   19.14  definition new' where
   19.15    [code del]: "new' = Array.new o Code_Numeral.nat_of"
   19.16 -hide (open) const new'
   19.17 +hide_const (open) new'
   19.18  lemma [code]:
   19.19    "Array.new = Array.new' o Code_Numeral.of_nat"
   19.20    by (simp add: new'_def o_def)
   19.21  
   19.22  definition of_list' where
   19.23    [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
   19.24 -hide (open) const of_list'
   19.25 +hide_const (open) of_list'
   19.26  lemma [code]:
   19.27    "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
   19.28    by (simp add: of_list'_def)
   19.29  
   19.30  definition make' where
   19.31    [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
   19.32 -hide (open) const make'
   19.33 +hide_const (open) make'
   19.34  lemma [code]:
   19.35    "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
   19.36    by (simp add: make'_def o_def)
   19.37  
   19.38  definition length' where
   19.39    [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
   19.40 -hide (open) const length'
   19.41 +hide_const (open) length'
   19.42  lemma [code]:
   19.43    "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
   19.44    by (simp add: length'_def monad_simp',
   19.45 @@ -145,14 +145,14 @@
   19.46  
   19.47  definition nth' where
   19.48    [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
   19.49 -hide (open) const nth'
   19.50 +hide_const (open) nth'
   19.51  lemma [code]:
   19.52    "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
   19.53    by (simp add: nth'_def)
   19.54  
   19.55  definition upd' where
   19.56    [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
   19.57 -hide (open) const upd'
   19.58 +hide_const (open) upd'
   19.59  lemma [code]:
   19.60    "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
   19.61    by (simp add: upd'_def monad_simp upd_return)
    20.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Fri Apr 16 20:56:40 2010 +0200
    20.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Apr 16 21:28:09 2010 +0200
    20.3 @@ -432,6 +432,6 @@
    20.4    "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
    20.5    by (simp add: array_present_def new_ref_def ref_def Let_def)
    20.6  
    20.7 -hide (open) const empty array array_of_list upd length ref
    20.8 +hide_const (open) empty array array_of_list upd length ref
    20.9  
   20.10  end
    21.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Apr 16 20:56:40 2010 +0200
    21.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Apr 16 21:28:09 2010 +0200
    21.3 @@ -405,7 +405,7 @@
    21.4  lemmas MREC_rule = mrec.MREC_rule
    21.5  lemmas MREC_pinduct = mrec.MREC_pinduct
    21.6  
    21.7 -hide (open) const heap execute
    21.8 +hide_const (open) heap execute
    21.9  
   21.10  
   21.11  subsection {* Code generator setup *}
   21.12 @@ -426,7 +426,7 @@
   21.13    "raise s = raise_exc (Fail (STR s))"
   21.14    unfolding Fail_def raise_exc_def raise_def ..
   21.15  
   21.16 -hide (open) const Fail raise_exc
   21.17 +hide_const (open) Fail raise_exc
   21.18  
   21.19  
   21.20  subsubsection {* SML and OCaml *}
    22.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Fri Apr 16 20:56:40 2010 +0200
    22.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Apr 16 21:28:09 2010 +0200
    22.3 @@ -41,7 +41,7 @@
    22.4                      return y
    22.5                   done)"
    22.6  
    22.7 -hide (open) const new lookup update change
    22.8 +hide_const (open) new lookup update change
    22.9  
   22.10  
   22.11  subsection {* Properties *}
    23.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Apr 16 20:56:40 2010 +0200
    23.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Apr 16 21:28:09 2010 +0200
    23.3 @@ -8,7 +8,7 @@
    23.4  imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray
    23.5  begin
    23.6  
    23.7 -hide (open) const swap rev
    23.8 +hide_const (open) swap rev
    23.9  
   23.10  fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
   23.11    "swap a i j = (do
    24.1 --- a/src/HOL/Int.thy	Fri Apr 16 20:56:40 2010 +0200
    24.2 +++ b/src/HOL/Int.thy	Fri Apr 16 21:28:09 2010 +0200
    24.3 @@ -2263,7 +2263,7 @@
    24.4  lemma [code]: "nat i = nat_aux i 0"
    24.5    by (simp add: nat_aux_def)
    24.6  
    24.7 -hide (open) const nat_aux
    24.8 +hide_const (open) nat_aux
    24.9  
   24.10  lemma zero_is_num_zero [code, code_unfold_post]:
   24.11    "(0\<Colon>int) = Numeral0" 
   24.12 @@ -2325,7 +2325,7 @@
   24.13  
   24.14  quickcheck_params [default_type = int]
   24.15  
   24.16 -hide (open) const Pls Min Bit0 Bit1 succ pred
   24.17 +hide_const (open) Pls Min Bit0 Bit1 succ pred
   24.18  
   24.19  
   24.20  subsection {* Legacy theorems *}
    25.1 --- a/src/HOL/Lattice/Bounds.thy	Fri Apr 16 20:56:40 2010 +0200
    25.2 +++ b/src/HOL/Lattice/Bounds.thy	Fri Apr 16 21:28:09 2010 +0200
    25.3 @@ -6,7 +6,7 @@
    25.4  
    25.5  theory Bounds imports Orders begin
    25.6  
    25.7 -hide (open) const inf sup
    25.8 +hide_const (open) inf sup
    25.9  
   25.10  subsection {* Infimum and supremum *}
   25.11  
    26.1 --- a/src/HOL/Lazy_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
    26.2 +++ b/src/HOL/Lazy_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
    26.3 @@ -212,8 +212,8 @@
    26.4  where
    26.5    "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
    26.6  
    26.7 -hide (open) type lazy_sequence
    26.8 -hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
    26.9 -hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
   26.10 +hide_type (open) lazy_sequence
   26.11 +hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
   26.12 +hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
   26.13  
   26.14  end
    27.1 --- a/src/HOL/Library/Dlist.thy	Fri Apr 16 20:56:40 2010 +0200
    27.2 +++ b/src/HOL/Library/Dlist.thy	Fri Apr 16 21:28:09 2010 +0200
    27.3 @@ -247,6 +247,6 @@
    27.4  
    27.5  end
    27.6  
    27.7 -hide (open) const member fold empty insert remove map filter null member length fold
    27.8 +hide_const (open) member fold empty insert remove map filter null member length fold
    27.9  
   27.10  end
    28.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Apr 16 20:56:40 2010 +0200
    28.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Apr 16 21:28:09 2010 +0200
    28.3 @@ -496,6 +496,6 @@
    28.4  code_modulename Haskell
    28.5    Efficient_Nat Arith
    28.6  
    28.7 -hide const int
    28.8 +hide_const int
    28.9  
   28.10  end
    29.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Apr 16 20:56:40 2010 +0200
    29.2 +++ b/src/HOL/Library/Executable_Set.thy	Fri Apr 16 21:28:09 2010 +0200
    29.3 @@ -265,7 +265,7 @@
    29.4    "Union (Coset []) = Coset []"
    29.5    unfolding Union_def Sup_sup by simp_all
    29.6  
    29.7 -hide (open) const is_empty empty remove
    29.8 +hide_const (open) is_empty empty remove
    29.9    set_eq subset_eq subset inter union subtract Inf Sup Inter Union
   29.10  
   29.11  end
    30.1 --- a/src/HOL/Library/Fset.thy	Fri Apr 16 20:56:40 2010 +0200
    30.2 +++ b/src/HOL/Library/Fset.thy	Fri Apr 16 21:28:09 2010 +0200
    30.3 @@ -293,7 +293,7 @@
    30.4  declare mem_def [simp del]
    30.5  
    30.6  
    30.7 -hide (open) const is_empty insert remove map filter forall exists card
    30.8 +hide_const (open) is_empty insert remove map filter forall exists card
    30.9    Inter Union
   30.10  
   30.11  end
    31.1 --- a/src/HOL/Library/Mapping.thy	Fri Apr 16 20:56:40 2010 +0200
    31.2 +++ b/src/HOL/Library/Mapping.thy	Fri Apr 16 21:28:09 2010 +0200
    31.3 @@ -146,6 +146,6 @@
    31.4    by (cases m) simp
    31.5  
    31.6  
    31.7 -hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
    31.8 +hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
    31.9  
   31.10  end
   31.11 \ No newline at end of file
    32.1 --- a/src/HOL/Library/Multiset.thy	Fri Apr 16 20:56:40 2010 +0200
    32.2 +++ b/src/HOL/Library/Multiset.thy	Fri Apr 16 21:28:09 2010 +0200
    32.3 @@ -1001,7 +1001,7 @@
    32.4  no_notation fcomp (infixl "o>" 60)
    32.5  no_notation scomp (infixl "o\<rightarrow>" 60)
    32.6  
    32.7 -hide (open) const bagify
    32.8 +hide_const (open) bagify
    32.9  
   32.10  
   32.11  subsection {* The multiset order *}
    33.1 --- a/src/HOL/Library/Nested_Environment.thy	Fri Apr 16 20:56:40 2010 +0200
    33.2 +++ b/src/HOL/Library/Nested_Environment.thy	Fri Apr 16 21:28:09 2010 +0200
    33.3 @@ -54,7 +54,7 @@
    33.4    | "lookup_option None xs = None"
    33.5    | "lookup_option (Some e) xs = lookup e xs"
    33.6  
    33.7 -hide const lookup_option
    33.8 +hide_const lookup_option
    33.9  
   33.10  text {*
   33.11    \medskip The characteristic cases of @{term lookup} are expressed by
   33.12 @@ -262,7 +262,7 @@
   33.13    | "update_option xs opt (Some e) =
   33.14        (if xs = [] then opt else Some (update xs opt e))"
   33.15  
   33.16 -hide const update_option
   33.17 +hide_const update_option
   33.18  
   33.19  text {*
   33.20    \medskip The characteristic cases of @{term update} are expressed by
    34.1 --- a/src/HOL/Library/RBT.thy	Fri Apr 16 20:56:40 2010 +0200
    34.2 +++ b/src/HOL/Library/RBT.thy	Fri Apr 16 21:28:09 2010 +0200
    34.3 @@ -224,7 +224,7 @@
    34.4    "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
    34.5    by (simp add: eq Mapping_def entries_lookup)
    34.6  
    34.7 -hide (open) const impl_of lookup empty insert delete
    34.8 +hide_const (open) impl_of lookup empty insert delete
    34.9    entries keys bulkload map_entry map fold
   34.10  (*>*)
   34.11  
    35.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Apr 16 20:56:40 2010 +0200
    35.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Apr 16 21:28:09 2010 +0200
    35.3 @@ -1079,6 +1079,6 @@
    35.4    then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
    35.5  qed
    35.6  
    35.7 -hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
    35.8 +hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
    35.9  
   35.10  end
    36.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Fri Apr 16 20:56:40 2010 +0200
    36.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri Apr 16 21:28:09 2010 +0200
    36.3 @@ -227,8 +227,8 @@
    36.4  value "test\<^sup>*\<^sup>* A C"
    36.5  value "test\<^sup>*\<^sup>* C A"
    36.6  
    36.7 -hide type ty
    36.8 -hide const test A B C
    36.9 +hide_type ty
   36.10 +hide_const test A B C
   36.11  
   36.12  end
   36.13  
    37.1 --- a/src/HOL/List.thy	Fri Apr 16 20:56:40 2010 +0200
    37.2 +++ b/src/HOL/List.thy	Fri Apr 16 21:28:09 2010 +0200
    37.3 @@ -172,7 +172,8 @@
    37.4    insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    37.5    "insert x xs = (if x \<in> set xs then xs else x # xs)"
    37.6  
    37.7 -hide (open) const insert hide (open) fact insert_def
    37.8 +hide_const (open) insert
    37.9 +hide_fact (open) insert_def
   37.10  
   37.11  primrec
   37.12    remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   37.13 @@ -4584,7 +4585,7 @@
   37.14  
   37.15  declare set_map [symmetric, code_unfold]
   37.16  
   37.17 -hide (open) const length_unique
   37.18 +hide_const (open) length_unique
   37.19  
   37.20  
   37.21  text {* Code for bounded quantification and summation over nats. *}
    38.1 --- a/src/HOL/NSA/Filter.thy	Fri Apr 16 20:56:40 2010 +0200
    38.2 +++ b/src/HOL/NSA/Filter.thy	Fri Apr 16 21:28:09 2010 +0200
    38.3 @@ -403,6 +403,6 @@
    38.4  
    38.5  lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
    38.6  
    38.7 -hide (open) const filter
    38.8 +hide_const (open) filter
    38.9  
   38.10  end
    39.1 --- a/src/HOL/Nat.thy	Fri Apr 16 20:56:40 2010 +0200
    39.2 +++ b/src/HOL/Nat.thy	Fri Apr 16 21:28:09 2010 +0200
    39.3 @@ -175,7 +175,7 @@
    39.4  
    39.5  end
    39.6  
    39.7 -hide (open) fact add_0 add_0_right diff_0
    39.8 +hide_fact (open) add_0 add_0_right diff_0
    39.9  
   39.10  instantiation nat :: comm_semiring_1_cancel
   39.11  begin
   39.12 @@ -1212,7 +1212,7 @@
   39.13    "funpow (Suc n) f = f o funpow n f"
   39.14    unfolding funpow_code_def by simp_all
   39.15  
   39.16 -hide (open) const funpow
   39.17 +hide_const (open) funpow
   39.18  
   39.19  lemma funpow_add:
   39.20    "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
   39.21 @@ -1504,7 +1504,7 @@
   39.22  lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
   39.23  by (simp split add: nat_diff_split)
   39.24  
   39.25 -hide (open) fact diff_diff_eq
   39.26 +hide_fact (open) diff_diff_eq
   39.27  
   39.28  lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
   39.29  by (auto split add: nat_diff_split)
    40.1 --- a/src/HOL/New_DSequence.thy	Fri Apr 16 20:56:40 2010 +0200
    40.2 +++ b/src/HOL/New_DSequence.thy	Fri Apr 16 21:28:09 2010 +0200
    40.3 @@ -91,12 +91,12 @@
    40.4      None => Lazy_Sequence.hb_single ()
    40.5    | Some ((), xq) => Lazy_Sequence.empty)"
    40.6  
    40.7 -hide (open) type pos_dseq neg_dseq
    40.8 +hide_type (open) pos_dseq neg_dseq
    40.9  
   40.10 -hide (open) const 
   40.11 +hide_const (open)
   40.12    pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
   40.13    neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
   40.14 -hide (open) fact
   40.15 +hide_fact (open)
   40.16    pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def
   40.17    neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
   40.18  
    41.1 --- a/src/HOL/New_Random_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
    41.2 +++ b/src/HOL/New_Random_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
    41.3 @@ -91,16 +91,16 @@
    41.4  where
    41.5    "neg_map f P = neg_bind P (neg_single o f)"
    41.6  (*
    41.7 -hide const DSequence.empty DSequence.single DSequence.eval
    41.8 +hide_const DSequence.empty DSequence.single DSequence.eval
    41.9    DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
   41.10    DSequence.map
   41.11  *)
   41.12  
   41.13 -hide (open) const
   41.14 +hide_const (open)
   41.15    pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
   41.16    neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
   41.17 -hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
   41.18 +hide_type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
   41.19  (* FIXME: hide facts *)
   41.20 -(*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
   41.21 +(*hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
   41.22  
   41.23  end
   41.24 \ No newline at end of file
    42.1 --- a/src/HOL/Nitpick.thy	Fri Apr 16 20:56:40 2010 +0200
    42.2 +++ b/src/HOL/Nitpick.thy	Fri Apr 16 21:28:09 2010 +0200
    42.3 @@ -237,15 +237,15 @@
    42.4  
    42.5  setup {* Nitpick_Isar.setup *}
    42.6  
    42.7 -hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    42.8 +hide_const (open) unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    42.9      bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl'
   42.10      wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
   42.11      int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
   42.12      norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
   42.13      less_eq_frac of_frac
   42.14 -hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
   42.15 +hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
   42.16      word
   42.17 -hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
   42.18 +hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
   42.19      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
   42.20      The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
   42.21      nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    43.1 --- a/src/HOL/Option.thy	Fri Apr 16 20:56:40 2010 +0200
    43.2 +++ b/src/HOL/Option.thy	Fri Apr 16 21:28:09 2010 +0200
    43.3 @@ -82,7 +82,7 @@
    43.4    by (rule ext) (simp split: sum.split)
    43.5  
    43.6  
    43.7 -hide (open) const set map
    43.8 +hide_const (open) set map
    43.9  
   43.10  subsubsection {* Code generator setup *}
   43.11  
   43.12 @@ -102,7 +102,7 @@
   43.13    "eq_class.eq x None \<longleftrightarrow> is_none x"
   43.14    by (simp add: eq is_none_none)
   43.15  
   43.16 -hide (open) const is_none
   43.17 +hide_const (open) is_none
   43.18  
   43.19  code_type option
   43.20    (SML "_ option")
    44.1 --- a/src/HOL/Predicate.thy	Fri Apr 16 20:56:40 2010 +0200
    44.2 +++ b/src/HOL/Predicate.thy	Fri Apr 16 21:28:09 2010 +0200
    44.3 @@ -934,8 +934,8 @@
    44.4    bot ("\<bottom>") and
    44.5    bind (infixl "\<guillemotright>=" 70)
    44.6  
    44.7 -hide (open) type pred seq
    44.8 -hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
    44.9 +hide_type (open) pred seq
   44.10 +hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
   44.11    Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
   44.12  
   44.13  end
    45.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Apr 16 20:56:40 2010 +0200
    45.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Apr 16 21:28:09 2010 +0200
    45.3 @@ -1168,7 +1168,7 @@
    45.4  
    45.5  code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
    45.6  
    45.7 -hide const a b
    45.8 +hide_const a b
    45.9  
   45.10  subsection {* Lambda *}
   45.11  
    46.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Apr 16 20:56:40 2010 +0200
    46.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Apr 16 21:28:09 2010 +0200
    46.3 @@ -150,7 +150,7 @@
    46.4  quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
    46.5  oops
    46.6  
    46.7 -hide const a b
    46.8 +hide_const a b
    46.9  
   46.10  subsection {* Lexicographic order *}
   46.11  (* TODO *)
    47.1 --- a/src/HOL/Product_Type.thy	Fri Apr 16 20:56:40 2010 +0200
    47.2 +++ b/src/HOL/Product_Type.thy	Fri Apr 16 21:28:09 2010 +0200
    47.3 @@ -637,7 +637,7 @@
    47.4  use "Tools/split_rule.ML"
    47.5  setup Split_Rule.setup
    47.6  
    47.7 -hide const internal_split
    47.8 +hide_const internal_split
    47.9  
   47.10  
   47.11  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
    48.1 --- a/src/HOL/Quickcheck.thy	Fri Apr 16 20:56:40 2010 +0200
    48.2 +++ b/src/HOL/Quickcheck.thy	Fri Apr 16 21:28:09 2010 +0200
    48.3 @@ -203,9 +203,9 @@
    48.4  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
    48.5    where "map f P = bind P (single o f)"
    48.6  
    48.7 -hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
    48.8 -hide (open) type randompred
    48.9 -hide (open) const random collapse beyond random_fun_aux random_fun_lift
   48.10 +hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
   48.11 +hide_type (open) randompred
   48.12 +hide_const (open) random collapse beyond random_fun_aux random_fun_lift
   48.13    iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
   48.14  
   48.15  end
    49.1 --- a/src/HOL/Random.thy	Fri Apr 16 20:56:40 2010 +0200
    49.2 +++ b/src/HOL/Random.thy	Fri Apr 16 21:28:09 2010 +0200
    49.3 @@ -174,10 +174,10 @@
    49.4  end;
    49.5  *}
    49.6  
    49.7 -hide (open) type seed
    49.8 -hide (open) const inc_shift minus_shift log "next" split_seed
    49.9 +hide_type (open) seed
   49.10 +hide_const (open) inc_shift minus_shift log "next" split_seed
   49.11    iterate range select pick select_weight
   49.12 -hide (open) fact range_def
   49.13 +hide_fact (open) range_def
   49.14  
   49.15  no_notation fcomp (infixl "o>" 60)
   49.16  no_notation scomp (infixl "o\<rightarrow>" 60)
    50.1 --- a/src/HOL/Random_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
    50.2 +++ b/src/HOL/Random_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
    50.3 @@ -48,14 +48,14 @@
    50.4    "map f P = bind P (single o f)"
    50.5  
    50.6  (*
    50.7 -hide const DSequence.empty DSequence.single DSequence.eval
    50.8 +hide_const DSequence.empty DSequence.single DSequence.eval
    50.9    DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
   50.10    DSequence.map
   50.11  *)
   50.12  
   50.13 -hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
   50.14 +hide_const (open) empty single bind union if_random_dseq not_random_dseq Random map
   50.15  
   50.16 -hide type DSequence.dseq random_dseq
   50.17 -hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
   50.18 +hide_type DSequence.dseq random_dseq
   50.19 +hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
   50.20  
   50.21  end
   50.22 \ No newline at end of file
    51.1 --- a/src/HOL/Record.thy	Fri Apr 16 20:56:40 2010 +0200
    51.2 +++ b/src/HOL/Record.thy	Fri Apr 16 21:28:09 2010 +0200
    51.3 @@ -455,7 +455,7 @@
    51.4  use "Tools/record.ML"
    51.5  setup Record.setup
    51.6  
    51.7 -hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
    51.8 +hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
    51.9    iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   51.10    iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
   51.11    iso_tuple_update_accessor_eq_assist tuple_iso_tuple
    52.1 --- a/src/HOL/String.thy	Fri Apr 16 20:56:40 2010 +0200
    52.2 +++ b/src/HOL/String.thy	Fri Apr 16 21:28:09 2010 +0200
    52.3 @@ -217,6 +217,6 @@
    52.4  in Codegen.add_codegen "char_codegen" char_codegen end
    52.5  *}
    52.6  
    52.7 -hide (open) type literal
    52.8 +hide_type (open) literal
    52.9  
   52.10  end
   52.11 \ No newline at end of file
    53.1 --- a/src/HOL/Sum_Type.thy	Fri Apr 16 20:56:40 2010 +0200
    53.2 +++ b/src/HOL/Sum_Type.thy	Fri Apr 16 21:28:09 2010 +0200
    53.3 @@ -187,6 +187,6 @@
    53.4    show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
    53.5  qed
    53.6  
    53.7 -hide (open) const Suml Sumr Projl Projr
    53.8 +hide_const (open) Suml Sumr Projl Projr
    53.9  
   53.10  end
    54.1 --- a/src/HOL/Typerep.thy	Fri Apr 16 20:56:40 2010 +0200
    54.2 +++ b/src/HOL/Typerep.thy	Fri Apr 16 21:28:09 2010 +0200
    54.3 @@ -90,6 +90,6 @@
    54.4  
    54.5  code_reserved Eval Term
    54.6  
    54.7 -hide (open) const typerep Typerep
    54.8 +hide_const (open) typerep Typerep
    54.9  
   54.10  end
    55.1 --- a/src/HOL/Word/BinGeneral.thy	Fri Apr 16 20:56:40 2010 +0200
    55.2 +++ b/src/HOL/Word/BinGeneral.thy	Fri Apr 16 21:28:09 2010 +0200
    55.3 @@ -28,7 +28,7 @@
    55.4  
    55.5  lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
    55.6  
    55.7 -hide (open) const B0 B1
    55.8 +hide_const (open) B0 B1
    55.9  
   55.10  lemma Min_ne_Pls [iff]:  
   55.11    "Int.Min ~= Int.Pls"
    56.1 --- a/src/HOL/ex/Meson_Test.thy	Fri Apr 16 20:56:40 2010 +0200
    56.2 +++ b/src/HOL/ex/Meson_Test.thy	Fri Apr 16 21:28:09 2010 +0200
    56.3 @@ -16,7 +16,7 @@
    56.4    below and constants declared in HOL!
    56.5  *}
    56.6  
    56.7 -hide (open) const subset member quotient union inter
    56.8 +hide_const (open) subset member quotient union inter
    56.9  
   56.10  text {*
   56.11    Test data for the MESON proof procedure
    57.1 --- a/src/HOL/ex/Numeral.thy	Fri Apr 16 20:56:40 2010 +0200
    57.2 +++ b/src/HOL/ex/Numeral.thy	Fri Apr 16 21:28:09 2010 +0200
    57.3 @@ -879,7 +879,7 @@
    57.4  declare zero_is_num_zero [code_unfold del]
    57.5  declare one_is_num_one [code_unfold del]
    57.6  
    57.7 -hide (open) const sub dup
    57.8 +hide_const (open) sub dup
    57.9  
   57.10  
   57.11  subsection {* Numeral equations as default simplification rules *}
    58.1 --- a/src/HOL/ex/RPred.thy	Fri Apr 16 20:56:40 2010 +0200
    58.2 +++ b/src/HOL/ex/RPred.thy	Fri Apr 16 21:28:09 2010 +0200
    58.3 @@ -47,6 +47,6 @@
    58.4  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
    58.5    where "map f P = bind P (return o f)"
    58.6  
    58.7 -hide (open) const return bind supp map
    58.8 +hide_const (open) return bind supp map
    58.9    
   58.10  end
   58.11 \ No newline at end of file
    59.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Apr 16 20:56:40 2010 +0200
    59.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Apr 16 21:28:09 2010 +0200
    59.3 @@ -17,7 +17,7 @@
    59.4    iff_keep :: "[bool, bool] => bool"
    59.5    iff_unfold :: "[bool, bool] => bool"
    59.6  
    59.7 -hide const iff_keep iff_unfold
    59.8 +hide_const iff_keep iff_unfold
    59.9  
   59.10  oracle svc_oracle = Svc.oracle
   59.11  
    60.1 --- a/src/HOLCF/Fixrec.thy	Fri Apr 16 20:56:40 2010 +0200
    60.2 +++ b/src/HOLCF/Fixrec.thy	Fri Apr 16 21:28:09 2010 +0200
    60.3 @@ -608,7 +608,7 @@
    60.4        (@{const_name UU}, @{const_name match_UU}) ]
    60.5  *}
    60.6  
    60.7 -hide (open) const return bind fail run cases
    60.8 +hide_const (open) return bind fail run cases
    60.9  
   60.10  lemmas [fixrec_simp] =
   60.11    run_strict run_fail run_return
    61.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Fri Apr 16 20:56:40 2010 +0200
    61.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Fri Apr 16 21:28:09 2010 +0200
    61.3 @@ -59,7 +59,7 @@
    61.4  
    61.5    (* hiding and restricting *)
    61.6    hide_asig     :: "['a signature, 'a set] => 'a signature"
    61.7 -  "hide"        :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
    61.8 +  hide          :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
    61.9    restrict_asig :: "['a signature, 'a set] => 'a signature"
   61.10    restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
   61.11  
    62.1 --- a/src/HOLCF/Universal.thy	Fri Apr 16 20:56:40 2010 +0200
    62.2 +++ b/src/HOLCF/Universal.thy	Fri Apr 16 21:28:09 2010 +0200
    62.3 @@ -809,7 +809,7 @@
    62.4   apply (rule ubasis_until_less)
    62.5  done
    62.6  
    62.7 -hide (open) const
    62.8 +hide_const (open)
    62.9    node
   62.10    choose
   62.11    choose_pos
    63.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 20:56:40 2010 +0200
    63.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 21:28:09 2010 +0200
    63.3 @@ -20,7 +20,10 @@
    63.4    val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
    63.5    val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
    63.6      local_theory -> local_theory
    63.7 -  val hide_names: bool -> string * xstring list -> theory -> theory
    63.8 +  val hide_class: bool -> xstring list -> theory -> theory
    63.9 +  val hide_type: bool -> xstring list -> theory -> theory
   63.10 +  val hide_const: bool -> xstring list -> theory -> theory
   63.11 +  val hide_fact: bool -> xstring list -> theory -> theory
   63.12    val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   63.13    val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   63.14    val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   63.15 @@ -202,23 +205,19 @@
   63.16  
   63.17  (* hide names *)
   63.18  
   63.19 -val hide_kinds =
   63.20 - [("class", (Sign.intern_class, can o Sign.certify_class, Sign.hide_class)),
   63.21 -  ("type", (Sign.intern_type, Sign.declared_tyname, Sign.hide_type)),
   63.22 -  ("const", (Sign.intern_const, Sign.declared_const, Sign.hide_const)),
   63.23 -  ("fact", (PureThy.intern_fact, PureThy.defined_fact, PureThy.hide_fact))];
   63.24 +fun hide_names intern check hide fully xnames thy =
   63.25 +  let
   63.26 +    val names = map (intern thy) xnames;
   63.27 +    val bads = filter_out (check thy) names;
   63.28 +  in
   63.29 +    if null bads then fold (hide fully) names thy
   63.30 +    else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
   63.31 +  end;
   63.32  
   63.33 -fun hide_names b (kind, xnames) thy =
   63.34 -  (case AList.lookup (op =) hide_kinds kind of
   63.35 -    SOME (intern, check, hide) =>
   63.36 -      let
   63.37 -        val names = map (intern thy) xnames;
   63.38 -        val bads = filter_out (check thy) names;
   63.39 -      in
   63.40 -        if null bads then fold (hide b) names thy
   63.41 -        else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
   63.42 -      end
   63.43 -  | NONE => error ("Bad name space specification: " ^ quote kind));
   63.44 +val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
   63.45 +val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
   63.46 +val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
   63.47 +val hide_fact = hide_names PureThy.intern_fact PureThy.defined_fact PureThy.hide_fact;
   63.48  
   63.49  
   63.50  (* goals *)
    64.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 16 20:56:40 2010 +0200
    64.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 16 21:28:09 2010 +0200
    64.3 @@ -285,10 +285,15 @@
    64.4    OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
    64.5      (Scan.succeed (Toplevel.theory Sign.local_path));
    64.6  
    64.7 -val _ =
    64.8 -  OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
    64.9 -    ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
   64.10 -      (Toplevel.theory o uncurry IsarCmd.hide_names));
   64.11 +fun hide_names name hide what =
   64.12 +  OuterSyntax.command name ("hide " ^ what ^ " from name space") K.thy_decl
   64.13 +    ((P.opt_keyword "open" >> not) -- Scan.repeat1 P.xname >>
   64.14 +      (Toplevel.theory o uncurry hide));
   64.15 +
   64.16 +val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
   64.17 +val _ = hide_names "hide_type" IsarCmd.hide_type "types";
   64.18 +val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
   64.19 +val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
   64.20  
   64.21  
   64.22  (* use ML text *)