equal
deleted
inserted
replaced
327 else if not is_class then Locale.init target |
327 else if not is_class then Locale.init target |
328 else Class_Target.init target; |
328 else Class_Target.init target; |
329 |
329 |
330 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = |
330 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = |
331 Data.put ta #> |
331 Data.put ta #> |
332 LocalTheory.init (NameSpace.base_name target) |
332 LocalTheory.init (Long_Name.base_name target) |
333 {pretty = pretty ta, |
333 {pretty = pretty ta, |
334 abbrev = abbrev ta, |
334 abbrev = abbrev ta, |
335 define = define ta, |
335 define = define ta, |
336 notes = notes ta, |
336 notes = notes ta, |
337 type_syntax = type_syntax ta, |
337 type_syntax = type_syntax ta, |