equal
deleted
inserted
replaced
296 fun inject_name T = injectN ^"_"^encode_type T; |
296 fun inject_name T = injectN ^"_"^encode_type T; |
297 |
297 |
298 |
298 |
299 fun add_declaration name decl thy = |
299 fun add_declaration name decl thy = |
300 thy |
300 thy |
301 |> Named_Target.init name |
301 |> Named_Target.init NONE name |
302 |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy) |
302 |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy) |
303 |> Local_Theory.exit_global; |
303 |> Local_Theory.exit_global; |
304 |
304 |
305 fun parent_components thy (Ts, pname, renaming) = |
305 fun parent_components thy (Ts, pname, renaming) = |
306 let |
306 let |