src/Pure/Isar/theory_target.ML
changeset 30364 577edc39b501
parent 30344 10a67c5ddddb
child 30437 910a7aeb8dec
equal deleted inserted replaced
30363:9b8d9b6ef803 30364:577edc39b501
   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,