src/Pure/Isar/isar_syn.ML
changeset 38708 8915e3ce8655
parent 38379 67d71449e85b
child 38870 fb9f51ba1bbc
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 25 11:30:45 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 25 14:18:09 2010 +0200
     1.3 @@ -286,14 +286,6 @@
     1.4  
     1.5  (* name space entry path *)
     1.6  
     1.7 -val _ =
     1.8 -  Outer_Syntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
     1.9 -    (Scan.succeed (Toplevel.theory Sign.root_path));
    1.10 -
    1.11 -val _ =
    1.12 -  Outer_Syntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
    1.13 -    (Scan.succeed (Toplevel.theory Sign.local_path));
    1.14 -
    1.15  fun hide_names name hide what =
    1.16    Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
    1.17      ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>