src/Pure/Isar/generic_target.ML

     -> (Attrib.binding * (thm list * Args.src list) list) list
     -> (Attrib.binding * (thm list * Args.src list) list) list
     -> local_theory -> local_theory)
     -> string -> (Attrib.binding * (thm list * Args.src list) list) list
     -> local_theory -> (string * thm list) list * local_theory
-  val abbrev: (string * bool -> binding * mixfix -> term * term -> (string * sort) list * term list
-    -> local_theory -> local_theory)
-    -> string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
+  val abbrev: (string * bool -> binding * mixfix -> term * term
+    -> (string * sort) list * term list -> local_theory -> local_theory)
+    -> string * bool -> (binding * mixfix) * term -> local_theory
+    -> (term * term) * local_theory
 end;
 
 structure Generic_Target: GENERIC_TARGET =
 struct
 

     val cert = Thm.cterm_of thy;
 
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;
     val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
-    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
+    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume)
+      (Assumption.all_assms_of ctxt);
     val nprems = Thm.nprems_of th' - Thm.nprems_of th;
 
     (*export fixes*)
     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
     val frees = map Free (Thm.fold_terms Term.add_frees th' []);