src/HOL/Tools/lin_arith.ML

   Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
     "declaration of split rules for arithmetic procedure" #>
   Method.setup @{binding linarith}
     (Scan.succeed (fn ctxt =>
       METHOD (fn facts =>
-        HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
+        HEADGOAL
+          (Method.insert_tac ctxt
+            (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
           THEN' tac ctxt)))) "linear arithmetic" #>
   Arith_Data.add_tactic "linear arithmetic" tac;
 
 val setup =
   init_arith_data