equal
deleted
inserted
replaced
353 |
353 |
354 |
354 |
355 fun add_declaration name decl thy = |
355 fun add_declaration name decl thy = |
356 thy |
356 thy |
357 |> TheoryTarget.init name |
357 |> TheoryTarget.init name |
358 |> (fn lthy => LocalTheory.declaration (decl lthy) lthy) |
358 |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy) |
359 |> LocalTheory.exit_global; |
359 |> LocalTheory.exit_global; |
360 |
360 |
361 fun parent_components thy (Ts, pname, renaming) = |
361 fun parent_components thy (Ts, pname, renaming) = |
362 let |
362 let |
363 val ctxt = Context.Theory thy; |
363 val ctxt = Context.Theory thy; |