--- a/src/HOL/Tools/lin_arith.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Dec 13 21:56:15 2015 +0100
@@ -895,7 +895,9 @@
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;