src/HOL/Tools/Function/mutual.ML

   in
     F ctxt (f, qs, gs, args, rhs) import export
   end
 
 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
-  import (export : thm -> thm) sum_psimp_eq =
+    import (export : thm -> thm) sum_psimp_eq =
   let
     val (MutualPart {f=SOME f, ...}) = get_part fname parts
 
     val psimp = import sum_psimp_eq
     val (simp, restore_cond) =

       | _ => raise General.Fail "Too many conditions"
 
   in
     Goal.prove ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
-         THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
+      (fn _ =>
+        Local_Defs.unfold_tac ctxt all_orig_fdefs
+          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
+          THEN (simp_tac (simpset_of ctxt)) 1)
     |> restore_cond
     |> export
   end
 
 fun mk_applied_form ctxt caTs thm =