197 |> Proof_Context.init_global |
197 |> Proof_Context.init_global |
198 |> Data.put overloading |
198 |> Data.put overloading |
199 |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading |
199 |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading |
200 |> activate_improvable_syntax |
200 |> activate_improvable_syntax |
201 |> synchronize_syntax |
201 |> synchronize_syntax |
202 |> Local_Theory.init (Sign.naming_of thy) |
202 |> Local_Theory.init |
|
203 {background_naming = Sign.naming_of thy, |
|
204 exit = conclude #> Local_Theory.target_of #> Sign.change_end_local} |
203 {define = Generic_Target.define foundation, |
205 {define = Generic_Target.define foundation, |
204 notes = Generic_Target.notes Generic_Target.theory_target_notes, |
206 notes = Generic_Target.notes Generic_Target.theory_target_notes, |
205 abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev, |
207 abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev, |
206 declaration = K Generic_Target.theory_declaration, |
208 declaration = K Generic_Target.theory_declaration, |
207 theory_registration = Generic_Target.theory_registration, |
209 theory_registration = Generic_Target.theory_registration, |
208 locale_dependency = fn _ => error "Not possible in overloading target", |
210 locale_dependency = fn _ => error "Not possible in overloading target", |
209 pretty = pretty, |
211 pretty = pretty} |
210 exit = conclude #> Local_Theory.target_of #> Sign.change_end_local} |
|
211 end; |
212 end; |
212 |
213 |
213 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); |
214 val overloading_cmd = gen_overloading Syntax.read_term; |
215 val overloading_cmd = gen_overloading Syntax.read_term; |
215 |
216 |