IsarCmd.hide_names;
authorwenzelm
Tue, 15 Apr 2008 18:49:27 +0200
changeset 26672 f99956db6ccd
parent 26671 c95590e01df5
child 26673 cda3df424bad
IsarCmd.hide_names;
src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 15 18:49:26 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 15 18:49:27 2008 +0200
@@ -296,7 +296,7 @@
 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 Sign.hide_names));
+      (Toplevel.theory o uncurry IsarCmd.hide_names));
 
 
 (* use ML text *)