equal
deleted
inserted
replaced
204 notes = Generic_Target.notes |
204 notes = Generic_Target.notes |
205 (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), |
205 (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), |
206 abbrev = Generic_Target.abbrev |
206 abbrev = Generic_Target.abbrev |
207 (fn prmode => fn (b, mx) => fn (t, _) => fn _ => |
207 (fn prmode => fn (b, mx) => fn (t, _) => fn _ => |
208 Generic_Target.theory_abbrev prmode ((b, mx), t)), |
208 Generic_Target.theory_abbrev prmode ((b, mx), t)), |
209 declaration = K Generic_Target.theory_declaration, |
209 declaration = Generic_Target.theory_declaration o #syntax, |
210 pretty = pretty, |
210 pretty = pretty, |
211 exit = Local_Theory.target_of o conclude} |
211 exit = Local_Theory.target_of o conclude} |
212 end; |
212 end; |
213 |
213 |
214 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); |
214 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); |