equal
deleted
inserted
replaced
294 (Scan.succeed (Toplevel.theory Sign.local_path)); |
294 (Scan.succeed (Toplevel.theory Sign.local_path)); |
295 |
295 |
296 val _ = |
296 val _ = |
297 OuterSyntax.command "hide" "hide names from given name space" K.thy_decl |
297 OuterSyntax.command "hide" "hide names from given name space" K.thy_decl |
298 ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >> |
298 ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >> |
299 (Toplevel.theory o uncurry Sign.hide_names)); |
299 (Toplevel.theory o uncurry IsarCmd.hide_names)); |
300 |
300 |
301 |
301 |
302 (* use ML text *) |
302 (* use ML text *) |
303 |
303 |
304 val _ = |
304 val _ = |