tuned whitespace;

--- a/src/Pure/Isar/generic_target.ML	Wed May 13 17:27:12 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed May 13 17:36:33 2015 +0200
@@ -7,17 +7,17 @@
 
 signature GENERIC_TARGET =
 sig
-  (* consts *)
+  (*consts*)
   val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
 
-  (* background operations *)
+  (*background operations*)
   val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val background_declaration: declaration -> local_theory -> local_theory
   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
 
-  (* lifting primitives to local theory operations *)
+  (*lifting primitives to local theory operations*)
   val define: (((binding * typ) * mixfix) * (binding * term) ->
       term list * term list -> local_theory -> (term * thm) * local_theory) ->
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -31,7 +31,7 @@
       term list * term list -> local_theory -> local_theory) ->
     string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
 
-  (* theory operations *)
+  (*theory operations*)
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_notes: string ->
@@ -44,7 +44,7 @@
   val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
 
-  (* locale operations *)
+  (*locale operations*)
   val locale_notes: string -> string ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
@@ -75,6 +75,7 @@
     else ctxt) lthy;
 
 
+
 (** declarations **)
 
 fun standard_declaration pred decl lthy =
@@ -84,6 +85,7 @@
     else ctxt) lthy;
 
 
+
 (** consts **)
 
 fun check_mixfix ctxt (b, extra_tfrees) mx =
@@ -123,7 +125,7 @@
           | _ => NONE)
         else NONE;
     in
-      case const_alias of
+      (case const_alias of
         SOME c =>
           context
           |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c)
@@ -133,7 +135,7 @@
           |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
           |-> (fn (const as Const (c, _), _) => same_shape ?
                 (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
-                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))
+                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
     end
   else context;
 
@@ -141,6 +143,7 @@
   standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
 
 
+
 (** background primitives **)
 
 fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
@@ -170,6 +173,7 @@
   #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params))
 
 
+
 (** lifting primitive to local theory operations **)
 
 (* define *)
@@ -300,6 +304,7 @@
   end;
 
 
+
 (** theory operations **)
 
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
@@ -326,6 +331,7 @@
   Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
 
 
+
 (** locale operations **)
 
 fun locale_notes locale kind global_facts local_facts =