equal
deleted
inserted
replaced
583 |> Local_Theory.init naming |
583 |> Local_Theory.init naming |
584 {define = Generic_Target.define foundation, |
584 {define = Generic_Target.define foundation, |
585 notes = Generic_Target.notes Generic_Target.theory_notes, |
585 notes = Generic_Target.notes Generic_Target.theory_notes, |
586 abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev, |
586 abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev, |
587 declaration = K Generic_Target.theory_declaration, |
587 declaration = K Generic_Target.theory_declaration, |
|
588 subscription = Generic_Target.theory_registration, |
588 pretty = pretty, |
589 pretty = pretty, |
589 exit = conclude #> Local_Theory.target_of #> Sign.change_end_local} |
590 exit = conclude #> Local_Theory.target_of #> Sign.change_end_local} |
590 end; |
591 end; |
591 |
592 |
592 fun instantiation_cmd arities thy = |
593 fun instantiation_cmd arities thy = |