# HG changeset patch
# User haftmann
# Date 1449126656 -3600
# Node ID f9e05eab6e3c6d99e171c4f5abd396f54f003366
# Parent  57bb7da5c867c62b4b24fa8b9ba900792d7f63c2
tuned sections

diff -r 57bb7da5c867 -r f9e05eab6e3c src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Dec 02 19:14:57 2015 +0100
+++ b/src/Pure/Isar/named_target.ML	Thu Dec 03 08:10:56 2015 +0100
@@ -63,7 +63,7 @@
   | _ => NONE;
 
 
-(* define *)
+(* operations *)
 
 fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params =
   Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
@@ -79,34 +79,19 @@
   | foundation (locale, false) = locale_foundation locale
   | foundation (class, true) = class_foundation class;
 
-
-(* notes *)
-
 fun notes ("", _) = Generic_Target.theory_target_notes
   | notes (locale, _) = Generic_Target.locale_target_notes locale;
 
-
-(* abbrev *)
-
 fun abbrev ("", _) = Generic_Target.theory_abbrev
   | abbrev (locale, false) = Generic_Target.locale_abbrev locale
   | abbrev (class, true) = Class.abbrev class;
 
-
-(* declaration *)
-
 fun declaration ("", _) flags decl = Generic_Target.theory_declaration decl
   | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
 
-
-(* subscription *)
-
 fun subscription ("", _) = Generic_Target.theory_registration
   | subscription (locale, _) = Generic_Target.locale_dependency locale;
 
-
-(* pretty *)
-
 fun pretty (target, is_class) ctxt =
   if target = "" then
     [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,