# HG changeset patch
# User wenzelm
# Date 1271446089 -7200
# Node ID 3fe7e97ccca8ae520f1df00226f468d4d8157a0a
# Parent  5cec4ca719d1525dffec4d96298b0bde970a35be
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

diff -r 5cec4ca719d1 -r 3fe7e97ccca8 doc-src/Codegen/Thy/Program.thy
--- a/doc-src/Codegen/Thy/Program.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/Codegen/Thy/Program.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -430,7 +430,7 @@
 
 subsection {* Inductive Predicates *}
 (*<*)
-hide const append
+hide_const append
 
 inductive append
 where
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 doc-src/Locales/Locales/Examples.thy
--- a/doc-src/Locales/Locales/Examples.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/Locales/Locales/Examples.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -2,7 +2,7 @@
 imports Main
 begin
 
-hide %invisible const Lattices.lattice
+hide_const %invisible Lattices.lattice
 pretty_setmargin %invisible 65
 
 (*
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 doc-src/Locales/Locales/document/Examples.tex
--- a/doc-src/Locales/Locales/document/Examples.tex	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex	Fri Apr 16 21:28:09 2010 +0200
@@ -25,8 +25,8 @@
 \endisadeliminvisible
 %
 \isataginvisible
-\isacommand{hide}\isamarkupfalse%
-\ const\ Lattices{\isachardot}lattice\isanewline
+\isacommand{hide{\isacharunderscore}const}\isamarkupfalse%
+\ Lattices{\isachardot}lattice\isanewline
 \isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse%
 \ {\isadigit{6}}{\isadigit{5}}%
 \endisataginvisible
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 doc-src/TutorialI/Datatype/Nested.thy
--- a/doc-src/TutorialI/Datatype/Nested.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -11,7 +11,7 @@
 Consider the following model of terms
 where function symbols can be applied to a list of arguments:
 *}
-(*<*)hide const Var(*>*)
+(*<*)hide_const Var(*>*)
 datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
 
 text{*\noindent
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -138,7 +138,7 @@
 *}
 
 (*<*)
-hide const xor
+hide_const xor
 setup {* Sign.add_path "version1" *}
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
@@ -161,7 +161,7 @@
 *}
 
 (*<*)
-hide const xor
+hide_const xor
 setup {* Sign.add_path "version2" *}
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 doc-src/TutorialI/Misc/Option2.thy
--- a/doc-src/TutorialI/Misc/Option2.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -1,7 +1,7 @@
 (*<*)
 theory Option2 imports Main begin
-hide const None Some
-hide type option
+hide_const None Some
+hide_type option
 (*>*)
 
 text{*\indexbold{*option (type)}\indexbold{*None (constant)}%
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 doc-src/TutorialI/Types/Overloading.thy
--- a/doc-src/TutorialI/Types/Overloading.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -1,6 +1,6 @@
 (*<*)theory Overloading imports Main Setup begin
 
-hide (open) "class" plus (*>*)
+hide_class (open) plus (*>*)
 
 text {* Type classes allow \emph{overloading}; thus a constant may
 have multiple definitions at non-overlapping types. *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/FOL/FOL.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -371,7 +371,7 @@
 lemmas induct_rulify_fallback =
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
 
-hide const induct_forall induct_implies induct_equal induct_conj
+hide_const induct_forall induct_implies induct_equal induct_conj
 
 
 text {* Method setup. *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Bali/Basis.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -176,7 +176,7 @@
 
 section "sums"
 
-hide const In0 In1
+hide_const In0 In1
 
 notation sum_case  (infixr "'(+')"80)
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -9,7 +9,7 @@
 
 section "error free"
  
-hide const field
+hide_const field
 
 lemma error_free_halloc:
   assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -280,8 +280,8 @@
 end
 *}
 
-hide const dummy_term App valapp
-hide (open) const Const termify valtermify term_of term_of_num
+hide_const dummy_term App valapp
+hide_const (open) Const termify valtermify term_of term_of_num
 
 subsection {* Tracing of generated and evaluated code *}
 
@@ -301,7 +301,7 @@
 code_const "tracing :: String.literal => 'a => 'a"
   (Eval "Code'_Evaluation.tracing")
 
-hide (open) const tracing
+hide_const (open) tracing
 code_reserved Eval Code_Evaluation
 
 subsection {* Evaluation setup *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -278,7 +278,7 @@
   then show ?thesis by (auto simp add: int_of_def mult_ac)
 qed
 
-hide (open) const of_nat nat_of int_of
+hide_const (open) of_nat nat_of int_of
 
 subsubsection {* Lazy Evaluation of an indexed function *}
 
@@ -289,7 +289,7 @@
 
 termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
 
-hide (open) const iterate_upto
+hide_const (open) iterate_upto
 
 subsection {* Code generator setup *}
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/DSequence.thy
--- a/src/HOL/DSequence.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/DSequence.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -97,13 +97,13 @@
 
 code_reserved Eval DSequence
 (*
-hide type Sequence.seq
+hide_type Sequence.seq
 
-hide const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
+hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
   Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
 *)
-hide (open) const empty single eval map_seq bind union if_seq not_seq map
-hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def
+hide_const (open) empty single eval map_seq bind union if_seq not_seq map
+hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def
   if_seq_def not_seq_def map_def
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Datatype.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -512,8 +512,8 @@
 
 
 text {* hides popular names *}
-hide (open) type node item
-hide (open) const Push Node Atom Leaf Numb Lim Split Case
+hide_type (open) node item
+hide_const (open) Push Node Atom Leaf Numb Lim Split Case
 
 use "Tools/Datatype/datatype.ML"
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -513,7 +513,7 @@
 class finite =
   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
 setup {* Sign.parent_path *}
-hide const finite
+hide_const finite
 
 context finite
 begin
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Fun.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -525,7 +525,7 @@
 lemma bij_swap_iff: "bij (swap a b f) = bij f"
 by (simp add: bij_def)
 
-hide (open) const swap
+hide_const (open) swap
 
 
 subsection {* Inversion of injective functions *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Groups.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -88,7 +88,7 @@
 class one =
   fixes one  :: 'a  ("1")
 
-hide (open) const zero one
+hide_const (open) zero one
 
 syntax
   "_index1"  :: index    ("\<^sub>1")
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -1567,7 +1567,7 @@
 lemma [induct_simp]: "(x = x) = True" 
   by (rule simp_thms)
 
-hide const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
+hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
 
 use "~~/src/Tools/induct_tacs.ML"
 setup InductTacs.setup
@@ -1886,8 +1886,8 @@
   Nbe.add_const_alias @{thm equals_alias_cert}
 *}
 
-hide (open) const eq
-hide const eq
+hide_const (open) eq
+hide_const eq
 
 text {* Cases *}
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -92,7 +92,7 @@
      return a
    done)"
 
-hide (open) const new map -- {* avoid clashed with some popular names *}
+hide_const (open) new map -- {* avoid clashed with some popular names *}
 
 
 subsection {* Properties *}
@@ -115,28 +115,28 @@
 
 definition new' where
   [code del]: "new' = Array.new o Code_Numeral.nat_of"
-hide (open) const new'
+hide_const (open) new'
 lemma [code]:
   "Array.new = Array.new' o Code_Numeral.of_nat"
   by (simp add: new'_def o_def)
 
 definition of_list' where
   [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
-hide (open) const of_list'
+hide_const (open) of_list'
 lemma [code]:
   "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
   by (simp add: of_list'_def)
 
 definition make' where
   [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
-hide (open) const make'
+hide_const (open) make'
 lemma [code]:
   "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
   by (simp add: make'_def o_def)
 
 definition length' where
   [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
-hide (open) const length'
+hide_const (open) length'
 lemma [code]:
   "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
   by (simp add: length'_def monad_simp',
@@ -145,14 +145,14 @@
 
 definition nth' where
   [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
-hide (open) const nth'
+hide_const (open) nth'
 lemma [code]:
   "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
   by (simp add: nth'_def)
 
 definition upd' where
   [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
-hide (open) const upd'
+hide_const (open) upd'
 lemma [code]:
   "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
   by (simp add: upd'_def monad_simp upd_return)
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -432,6 +432,6 @@
   "array_present a h \<Longrightarrow> array_present a (snd (ref v h))"
   by (simp add: array_present_def new_ref_def ref_def Let_def)
 
-hide (open) const empty array array_of_list upd length ref
+hide_const (open) empty array array_of_list upd length ref
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -405,7 +405,7 @@
 lemmas MREC_rule = mrec.MREC_rule
 lemmas MREC_pinduct = mrec.MREC_pinduct
 
-hide (open) const heap execute
+hide_const (open) heap execute
 
 
 subsection {* Code generator setup *}
@@ -426,7 +426,7 @@
   "raise s = raise_exc (Fail (STR s))"
   unfolding Fail_def raise_exc_def raise_def ..
 
-hide (open) const Fail raise_exc
+hide_const (open) Fail raise_exc
 
 
 subsubsection {* SML and OCaml *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -41,7 +41,7 @@
                     return y
                  done)"
 
-hide (open) const new lookup update change
+hide_const (open) new lookup update change
 
 
 subsection {* Properties *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -8,7 +8,7 @@
 imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray
 begin
 
-hide (open) const swap rev
+hide_const (open) swap rev
 
 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
   "swap a i j = (do
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Int.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -2263,7 +2263,7 @@
 lemma [code]: "nat i = nat_aux i 0"
   by (simp add: nat_aux_def)
 
-hide (open) const nat_aux
+hide_const (open) nat_aux
 
 lemma zero_is_num_zero [code, code_unfold_post]:
   "(0\<Colon>int) = Numeral0" 
@@ -2325,7 +2325,7 @@
 
 quickcheck_params [default_type = int]
 
-hide (open) const Pls Min Bit0 Bit1 succ pred
+hide_const (open) Pls Min Bit0 Bit1 succ pred
 
 
 subsection {* Legacy theorems *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Lattice/Bounds.thy
--- a/src/HOL/Lattice/Bounds.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Lattice/Bounds.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -6,7 +6,7 @@
 
 theory Bounds imports Orders begin
 
-hide (open) const inf sup
+hide_const (open) inf sup
 
 subsection {* Infimum and supremum *}
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -212,8 +212,8 @@
 where
   "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
 
-hide (open) type lazy_sequence
-hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
-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
+hide_type (open) lazy_sequence
+hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
+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
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -247,6 +247,6 @@
 
 end
 
-hide (open) const member fold empty insert remove map filter null member length fold
+hide_const (open) member fold empty insert remove map filter null member length fold
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -496,6 +496,6 @@
 code_modulename Haskell
   Efficient_Nat Arith
 
-hide const int
+hide_const int
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -265,7 +265,7 @@
   "Union (Coset []) = Coset []"
   unfolding Union_def Sup_sup by simp_all
 
-hide (open) const is_empty empty remove
+hide_const (open) is_empty empty remove
   set_eq subset_eq subset inter union subtract Inf Sup Inter Union
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -293,7 +293,7 @@
 declare mem_def [simp del]
 
 
-hide (open) const is_empty insert remove map filter forall exists card
+hide_const (open) is_empty insert remove map filter forall exists card
   Inter Union
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -146,6 +146,6 @@
   by (cases m) simp
 
 
-hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
+hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
 
 end
\ No newline at end of file
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -1001,7 +1001,7 @@
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)
 
-hide (open) const bagify
+hide_const (open) bagify
 
 
 subsection {* The multiset order *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -54,7 +54,7 @@
   | "lookup_option None xs = None"
   | "lookup_option (Some e) xs = lookup e xs"
 
-hide const lookup_option
+hide_const lookup_option
 
 text {*
   \medskip The characteristic cases of @{term lookup} are expressed by
@@ -262,7 +262,7 @@
   | "update_option xs opt (Some e) =
       (if xs = [] then opt else Some (update xs opt e))"
 
-hide const update_option
+hide_const update_option
 
 text {*
   \medskip The characteristic cases of @{term update} are expressed by
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/RBT.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -224,7 +224,7 @@
   "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
   by (simp add: eq Mapping_def entries_lookup)
 
-hide (open) const impl_of lookup empty insert delete
+hide_const (open) impl_of lookup empty insert delete
   entries keys bulkload map_entry map fold
 (*>*)
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -1079,6 +1079,6 @@
   then show ?thesis by (simp add: bulkload_def foldl_foldr lookup_Empty split_def)
 qed
 
-hide (open) const Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
+hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Library/Transitive_Closure_Table.thy
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -227,8 +227,8 @@
 value "test\<^sup>*\<^sup>* A C"
 value "test\<^sup>*\<^sup>* C A"
 
-hide type ty
-hide const test A B C
+hide_type ty
+hide_const test A B C
 
 end
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/List.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -172,7 +172,8 @@
   insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "insert x xs = (if x \<in> set xs then xs else x # xs)"
 
-hide (open) const insert hide (open) fact insert_def
+hide_const (open) insert
+hide_fact (open) insert_def
 
 primrec
   remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -4584,7 +4585,7 @@
 
 declare set_map [symmetric, code_unfold]
 
-hide (open) const length_unique
+hide_const (open) length_unique
 
 
 text {* Code for bounded quantification and summation over nats. *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/NSA/Filter.thy
--- a/src/HOL/NSA/Filter.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/NSA/Filter.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -403,6 +403,6 @@
 
 lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
 
-hide (open) const filter
+hide_const (open) filter
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Nat.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -175,7 +175,7 @@
 
 end
 
-hide (open) fact add_0 add_0_right diff_0
+hide_fact (open) add_0 add_0_right diff_0
 
 instantiation nat :: comm_semiring_1_cancel
 begin
@@ -1212,7 +1212,7 @@
   "funpow (Suc n) f = f o funpow n f"
   unfolding funpow_code_def by simp_all
 
-hide (open) const funpow
+hide_const (open) funpow
 
 lemma funpow_add:
   "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
@@ -1504,7 +1504,7 @@
 lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
 by (simp split add: nat_diff_split)
 
-hide (open) fact diff_diff_eq
+hide_fact (open) diff_diff_eq
 
 lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
 by (auto split add: nat_diff_split)
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/New_DSequence.thy
--- a/src/HOL/New_DSequence.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/New_DSequence.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -91,12 +91,12 @@
     None => Lazy_Sequence.hb_single ()
   | Some ((), xq) => Lazy_Sequence.empty)"
 
-hide (open) type pos_dseq neg_dseq
+hide_type (open) pos_dseq neg_dseq
 
-hide (open) const 
+hide_const (open)
   pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
   neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
-hide (open) fact
+hide_fact (open)
   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
   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
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/New_Random_Sequence.thy
--- a/src/HOL/New_Random_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/New_Random_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -91,16 +91,16 @@
 where
   "neg_map f P = neg_bind P (neg_single o f)"
 (*
-hide const DSequence.empty DSequence.single DSequence.eval
+hide_const DSequence.empty DSequence.single DSequence.eval
   DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
   DSequence.map
 *)
 
-hide (open) const
+hide_const (open)
   pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
   neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
-hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
+hide_type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
 (* FIXME: hide facts *)
-(*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
+(*hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
 
 end
\ No newline at end of file
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Nitpick.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -237,15 +237,15 @@
 
 setup {* Nitpick_Isar.setup *}
 
-hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
+hide_const (open) unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
     bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl'
     wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
     int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
     norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
     less_eq_frac of_frac
-hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
+hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
     word
-hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
+hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
     wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
     The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
     nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Option.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -82,7 +82,7 @@
   by (rule ext) (simp split: sum.split)
 
 
-hide (open) const set map
+hide_const (open) set map
 
 subsubsection {* Code generator setup *}
 
@@ -102,7 +102,7 @@
   "eq_class.eq x None \<longleftrightarrow> is_none x"
   by (simp add: eq is_none_none)
 
-hide (open) const is_none
+hide_const (open) is_none
 
 code_type option
   (SML "_ option")
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Predicate.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -934,8 +934,8 @@
   bot ("\<bottom>") and
   bind (infixl "\<guillemotright>=" 70)
 
-hide (open) type pred seq
-hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
+hide_type (open) pred seq
+hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -1168,7 +1168,7 @@
 
 code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
 
-hide const a b
+hide_const a b
 
 subsection {* Lambda *}
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -150,7 +150,7 @@
 quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
 oops
 
-hide const a b
+hide_const a b
 
 subsection {* Lexicographic order *}
 (* TODO *)
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Product_Type.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -637,7 +637,7 @@
 use "Tools/split_rule.ML"
 setup Split_Rule.setup
 
-hide const internal_split
+hide_const internal_split
 
 
 lemmas prod_caseI = prod.cases [THEN iffD2, standard]
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Quickcheck.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -203,9 +203,9 @@
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
   where "map f P = bind P (single o f)"
 
-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
-hide (open) type randompred
-hide (open) const random collapse beyond random_fun_aux random_fun_lift
+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
+hide_type (open) randompred
+hide_const (open) random collapse beyond random_fun_aux random_fun_lift
   iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Random.thy
--- a/src/HOL/Random.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Random.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -174,10 +174,10 @@
 end;
 *}
 
-hide (open) type seed
-hide (open) const inc_shift minus_shift log "next" split_seed
+hide_type (open) seed
+hide_const (open) inc_shift minus_shift log "next" split_seed
   iterate range select pick select_weight
-hide (open) fact range_def
+hide_fact (open) range_def
 
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Random_Sequence.thy
--- a/src/HOL/Random_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Random_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -48,14 +48,14 @@
   "map f P = bind P (single o f)"
 
 (*
-hide const DSequence.empty DSequence.single DSequence.eval
+hide_const DSequence.empty DSequence.single DSequence.eval
   DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
   DSequence.map
 *)
 
-hide (open) const empty single bind union if_random_dseq not_random_dseq Random map
+hide_const (open) empty single bind union if_random_dseq not_random_dseq Random map
 
-hide type DSequence.dseq random_dseq
-hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
+hide_type DSequence.dseq random_dseq
+hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
 
 end
\ No newline at end of file
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Record.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -455,7 +455,7 @@
 use "Tools/record.ML"
 setup Record.setup
 
-hide (open) const Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
+hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
   iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
   iso_tuple_update_accessor_eq_assist tuple_iso_tuple
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/String.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -217,6 +217,6 @@
 in Codegen.add_codegen "char_codegen" char_codegen end
 *}
 
-hide (open) type literal
+hide_type (open) literal
 
 end
\ No newline at end of file
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Sum_Type.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -187,6 +187,6 @@
   show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
 qed
 
-hide (open) const Suml Sumr Projl Projr
+hide_const (open) Suml Sumr Projl Projr
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Typerep.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -90,6 +90,6 @@
 
 code_reserved Eval Term
 
-hide (open) const typerep Typerep
+hide_const (open) typerep Typerep
 
 end
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -28,7 +28,7 @@
 
 lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
 
-hide (open) const B0 B1
+hide_const (open) B0 B1
 
 lemma Min_ne_Pls [iff]:  
   "Int.Min ~= Int.Pls"
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -16,7 +16,7 @@
   below and constants declared in HOL!
 *}
 
-hide (open) const subset member quotient union inter
+hide_const (open) subset member quotient union inter
 
 text {*
   Test data for the MESON proof procedure
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -879,7 +879,7 @@
 declare zero_is_num_zero [code_unfold del]
 declare one_is_num_one [code_unfold del]
 
-hide (open) const sub dup
+hide_const (open) sub dup
 
 
 subsection {* Numeral equations as default simplification rules *}
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/ex/RPred.thy
--- a/src/HOL/ex/RPred.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/ex/RPred.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -47,6 +47,6 @@
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
   where "map f P = bind P (return o f)"
 
-hide (open) const return bind supp map
+hide_const (open) return bind supp map
   
 end
\ No newline at end of file
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -17,7 +17,7 @@
   iff_keep :: "[bool, bool] => bool"
   iff_unfold :: "[bool, bool] => bool"
 
-hide const iff_keep iff_unfold
+hide_const iff_keep iff_unfold
 
 oracle svc_oracle = Svc.oracle
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOLCF/Fixrec.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -608,7 +608,7 @@
       (@{const_name UU}, @{const_name match_UU}) ]
 *}
 
-hide (open) const return bind fail run cases
+hide_const (open) return bind fail run cases
 
 lemmas [fixrec_simp] =
   run_strict run_fail run_return
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -59,7 +59,7 @@
 
   (* hiding and restricting *)
   hide_asig     :: "['a signature, 'a set] => 'a signature"
-  "hide"        :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+  hide          :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
   restrict_asig :: "['a signature, 'a set] => 'a signature"
   restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
 
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOLCF/Universal.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -809,7 +809,7 @@
  apply (rule ubasis_until_less)
 done
 
-hide (open) const
+hide_const (open)
   node
   choose
   choose_pos
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 21:28:09 2010 +0200
@@ -20,7 +20,10 @@
   val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
     local_theory -> local_theory
-  val hide_names: bool -> string * xstring list -> theory -> theory
+  val hide_class: bool -> xstring list -> theory -> theory
+  val hide_type: bool -> xstring list -> theory -> theory
+  val hide_const: bool -> xstring list -> theory -> theory
+  val hide_fact: bool -> xstring list -> theory -> theory
   val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -202,23 +205,19 @@
 
 (* hide names *)
 
-val hide_kinds =
- [("class", (Sign.intern_class, can o Sign.certify_class, Sign.hide_class)),
-  ("type", (Sign.intern_type, Sign.declared_tyname, Sign.hide_type)),
-  ("const", (Sign.intern_const, Sign.declared_const, Sign.hide_const)),
-  ("fact", (PureThy.intern_fact, PureThy.defined_fact, PureThy.hide_fact))];
+fun hide_names intern check hide fully xnames thy =
+  let
+    val names = map (intern thy) xnames;
+    val bads = filter_out (check thy) names;
+  in
+    if null bads then fold (hide fully) names thy
+    else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
+  end;
 
-fun hide_names b (kind, xnames) thy =
-  (case AList.lookup (op =) hide_kinds kind of
-    SOME (intern, check, hide) =>
-      let
-        val names = map (intern thy) xnames;
-        val bads = filter_out (check thy) names;
-      in
-        if null bads then fold (hide b) names thy
-        else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
-      end
-  | NONE => error ("Bad name space specification: " ^ quote kind));
+val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
+val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
+val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
+val hide_fact = hide_names PureThy.intern_fact PureThy.defined_fact PureThy.hide_fact;
 
 
 (* goals *)
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 16 21:28:09 2010 +0200
@@ -285,10 +285,15 @@
   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
     (Scan.succeed (Toplevel.theory Sign.local_path));
 
-val _ =
-  OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
-    ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
-      (Toplevel.theory o uncurry IsarCmd.hide_names));
+fun hide_names name hide what =
+  OuterSyntax.command name ("hide " ^ what ^ " from name space") K.thy_decl
+    ((P.opt_keyword "open" >> not) -- Scan.repeat1 P.xname >>
+      (Toplevel.theory o uncurry hide));
+
+val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
+val _ = hide_names "hide_type" IsarCmd.hide_type "types";
+val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
+val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
 
 
 (* use ML text *)