equal
deleted
inserted
replaced
558 notes = Generic_Target.notes |
558 notes = Generic_Target.notes |
559 (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), |
559 (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), |
560 abbrev = Generic_Target.abbrev |
560 abbrev = Generic_Target.abbrev |
561 (fn prmode => fn (b, mx) => fn (t, _) => fn _ => |
561 (fn prmode => fn (b, mx) => fn (t, _) => fn _ => |
562 Generic_Target.theory_abbrev prmode ((b, mx), t)), |
562 Generic_Target.theory_abbrev prmode ((b, mx), t)), |
563 declaration = K Generic_Target.theory_declaration, |
563 declaration = Generic_Target.theory_declaration o #syntax, |
564 pretty = pretty, |
564 pretty = pretty, |
565 exit = Local_Theory.target_of o conclude} |
565 exit = Local_Theory.target_of o conclude} |
566 end; |
566 end; |
567 |
567 |
568 fun instantiation_cmd arities thy = |
568 fun instantiation_cmd arities thy = |