# HG changeset patch
# User paulson
# Date 1014914806 -3600
# Node ID d796a2fd6c6904d03b861dd773fc89848cf93d28
# Parent  7acfab8361d1d7d32a04a7f208ee679ae93ee4c5
fixing nat_combine_numerals simprocs (again)

Theorem eq_cong2 moved from Integ/int_arith1.ML to simpdata.ML, where it will
be available in all theories.

Function simplify_meta_eq now makes the meta-equality first so that eq_cong2
will work properly.

diff -r 7acfab8361d1 -r d796a2fd6c69 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Thu Feb 28 17:21:48 2002 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Thu Feb 28 17:46:46 2002 +0100
@@ -70,11 +70,6 @@
                                      @zadd_ac@rel_iff_rel_0_rls) 1);
 qed "le_add_iff2";
 
-(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
-Goal "u = u' ==> (t==u) == (t==u')";
-by Auto_tac;
-qed "eq_cong2";
-
 
 structure Int_Numeral_Simprocs =
 struct
@@ -206,8 +201,8 @@
   | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
 
 fun simplify_meta_eq rules =
-    mk_meta_eq o
     simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
+    o mk_meta_eq;
 
 structure CancelNumeralsCommon =
   struct
diff -r 7acfab8361d1 -r d796a2fd6c69 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Feb 28 17:21:48 2002 +0100
+++ b/src/HOL/simpdata.ML	Thu Feb 28 17:46:46 2002 +0100
@@ -277,6 +277,11 @@
 by (etac arg_cong 1);
 qed "let_weak_cong";
 
+(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
+Goal "u = u' ==> (t==u) == (t==u')";
+by (asm_simp_tac HOL_ss 1);
+qed "eq_cong2";
+
 Goal "f(if c then x else y) = (if c then f x else f y)";
 by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
 qed "if_distrib";