src/Pure/sign.ML
changeset 71466 b1f3e86a4745
parent 71353 25b872d1d421
child 72283 4ed33ea8d957
equal deleted inserted replaced
71463:dd74e0558fd1 71466:b1f3e86a4745
   523 val mandatory_path = map_naming o Name_Space.mandatory_path;
   523 val mandatory_path = map_naming o Name_Space.mandatory_path;
   524 val qualified_path = map_naming oo Name_Space.qualified_path;
   524 val qualified_path = map_naming oo Name_Space.qualified_path;
   525 
   525 
   526 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   526 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   527 
   527 
   528 fun theory_naming thy = thy |> map_naming (Name_Space.set_theory_name (Context.theory_name thy));
   528 fun theory_naming thy = thy
       
   529   |> map_naming (Name_Space.set_theory_long_name (Context.theory_long_name thy));
   529 
   530 
   530 val private_scope = map_naming o Name_Space.private_scope;
   531 val private_scope = map_naming o Name_Space.private_scope;
   531 val private = map_naming o Name_Space.private;
   532 val private = map_naming o Name_Space.private;
   532 val qualified_scope = map_naming o Name_Space.qualified_scope;
   533 val qualified_scope = map_naming o Name_Space.qualified_scope;
   533 val qualified = map_naming o Name_Space.qualified;
   534 val qualified = map_naming o Name_Space.qualified;