equal
deleted
inserted
replaced
59 |
59 |
60 (* declaration *) |
60 (* declaration *) |
61 |
61 |
62 fun declare binding descr lthy = |
62 fun declare binding descr lthy = |
63 let |
63 let |
64 val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding; |
64 val name = Local_Theory.full_name lthy binding; |
65 val description = |
65 val description = |
66 "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); |
66 "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); |
67 val lthy' = lthy |
67 val lthy' = lthy |
68 |> Local_Theory.background_theory (Context.theory_map (new_entry name)) |
68 |> Local_Theory.background_theory (Context.theory_map (new_entry name)) |
69 |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) |
69 |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) |