equal
deleted
inserted
replaced
176 |
176 |
177 fun gen_method add_fixes name vars uses declares methods source lthy = |
177 fun gen_method add_fixes name vars uses declares methods source lthy = |
178 let |
178 let |
179 val (uses_internal, lthy1) = lthy |
179 val (uses_internal, lthy1) = lthy |
180 |> Proof_Context.concealed |
180 |> Proof_Context.concealed |
181 |> Local_Theory.open_target |-> Proof_Context.private_scope |
181 |> Local_Theory.begin_target |-> Proof_Context.private_scope |
182 |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name)) |
182 |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name)) |
183 |> Config.put Method.old_section_parser true |
183 |> Config.put Method.old_section_parser true |
184 |> fold setup_local_method methods |
184 |> fold setup_local_method methods |
185 |> fold_map (fn b => Named_Theorems.declare b "") uses; |
185 |> fold_map (fn b => Named_Theorems.declare b "") uses; |
186 |
186 |