src/Pure/Isar/class.ML
changeset 56723 a8f71445c265
parent 56334 6b3739fee456
child 57067 b3571d1a3e45
equal deleted inserted replaced
56722:ba1ac087b3a7 56723:a8f71445c265
   583     |> Local_Theory.init naming
   583     |> Local_Theory.init naming
   584        {define = Generic_Target.define foundation,
   584        {define = Generic_Target.define foundation,
   585         notes = Generic_Target.notes Generic_Target.theory_notes,
   585         notes = Generic_Target.notes Generic_Target.theory_notes,
   586         abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
   586         abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
   587         declaration = K Generic_Target.theory_declaration,
   587         declaration = K Generic_Target.theory_declaration,
       
   588         subscription = Generic_Target.theory_registration,
   588         pretty = pretty,
   589         pretty = pretty,
   589         exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   590         exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   590   end;
   591   end;
   591 
   592 
   592 fun instantiation_cmd arities thy =
   593 fun instantiation_cmd arities thy =