src/Pure/Isar/isar_syn.ML
changeset 36176 3fe7e97ccca8
parent 36174 feb6f24de47e
child 36178 0e5c133b48b6
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -285,10 +285,15 @@
     1.4    OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
     1.5      (Scan.succeed (Toplevel.theory Sign.local_path));
     1.6  
     1.7 -val _ =
     1.8 -  OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
     1.9 -    ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
    1.10 -      (Toplevel.theory o uncurry IsarCmd.hide_names));
    1.11 +fun hide_names name hide what =
    1.12 +  OuterSyntax.command name ("hide " ^ what ^ " from name space") K.thy_decl
    1.13 +    ((P.opt_keyword "open" >> not) -- Scan.repeat1 P.xname >>
    1.14 +      (Toplevel.theory o uncurry hide));
    1.15 +
    1.16 +val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
    1.17 +val _ = hide_names "hide_type" IsarCmd.hide_type "types";
    1.18 +val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
    1.19 +val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
    1.20  
    1.21  
    1.22  (* use ML text *)