changeset 57955 | f28337c2c0a8 |
parent 57952 | 1a9a6dfc255f |
child 58820 | 3ad2759acc52 |
--- a/src/HOL/Tools/arith_data.ML Sat Aug 16 16:18:39 2014 +0200 +++ b/src/HOL/Tools/arith_data.ML Sat Aug 16 16:45:39 2014 +0200 @@ -53,7 +53,7 @@ (Scan.succeed (fn ctxt => METHOD (fn facts => HEADGOAL - (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts) + (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts) THEN' verbose_arith_tac ctxt)))) "various arithmetic decision procedures";