src/Pure/Isar/named_target.ML

 
 
 (* declaration *)
 
 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
-  if target = "" then Generic_Target.standard_declaration decl lthy
+  if target = "" then Generic_Target.theory_declaration decl lthy
   else
     lthy
     |> pervasive ? Generic_Target.background_declaration decl
     |> Generic_Target.locale_declaration target syntax decl
     |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt =>