# HG changeset patch
# User wenzelm
# Date 1466518203 -7200
# Node ID fd9bd5024751dead71d650e2ba68d2844e70d435
# Parent  94c6e3ed0afb151a54dc5a7473226d88f38217a5
tuned whitespace;

diff -r 94c6e3ed0afb -r fd9bd5024751 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Jun 21 15:10:43 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Jun 21 16:10:03 2016 +0200
@@ -61,8 +61,8 @@
   (*locale target primitives*)
   val locale_target_notes: string -> string -> (Attrib.binding * Attrib.thms) list ->
     (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
-  val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
-    local_theory -> local_theory
+  val locale_target_abbrev: string -> Syntax.mode ->
+    (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
   val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
     (binding * mixfix) * term -> local_theory -> local_theory
@@ -90,7 +90,8 @@
     val rhs' = rhs
       |> Assumption.export_term lthy (Local_Theory.target_of lthy)
       |> preprocess;
-    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
+    val term_params =
+      map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
     val u = fold_rev lambda term_params rhs';
     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
 
@@ -351,7 +352,8 @@
   Local_Theory.background_theory_result
     (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
       (fn (lhs, _) =>  (* FIXME type_params!? *)
-        Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs))
+        Sign.notation true prmode
+          [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs))
   #-> (fn lhs =>
         standard_const (op <>) prmode
           ((b, if null (snd params) then NoSyn else mx),