# HG changeset patch
# User wenzelm
# Date 1130258301 -7200
# Node ID fa751791be4d1461c9921751b46a9ffe2af86fed
# Parent  47f81afce1b45181af291cbfbf93d8682697f4b6
EVERY;

diff -r 47f81afce1b4 -r fa751791be4d src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Tue Oct 25 18:18:59 2005 +0200
+++ b/src/HOL/arith_data.ML	Tue Oct 25 18:38:21 2005 +0200
@@ -51,7 +51,7 @@
 
 fun prove_conv expand_tac norm_tac sg ss tu =  (* FIXME avoid standard *)
   mk_meta_eq (standard (Goal.prove sg [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
-    (K [expand_tac, norm_tac ss])));
+    (K (EVERY [expand_tac, norm_tac ss]))));
 
 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
   (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);