src/HOL/Integ/NatSimprocs.ML
changeset 8785 00cff9d083df
parent 8776 60821dbc9f18
child 8787 9aeca9a34cf4
--- a/src/HOL/Integ/NatSimprocs.ML	Wed May 03 18:30:29 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Wed May 03 18:33:28 2000 +0200
@@ -76,9 +76,9 @@
 fun dest_numeral (Const ("0", _)) = 0
   | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
   | dest_numeral (Const("Numeral.number_of", _) $ w) = 
-        (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
-	 handle Match => raise TERM("dest_numeral:1", [w]))
-  | dest_numeral t = raise TERM("dest_numeral:2", [t]);
+      (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
+       handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
+  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
 
 fun find_first_numeral past (t::terms) =
 	((dest_numeral t, t, rev past @ terms)
@@ -175,9 +175,10 @@
   val find_first_coeff	= find_first_coeff []
   val subst_tac          = subst_tac
   val norm_tac = ALLGOALS
-                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@bin_simps@
+                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
                                        [add_0, Suc_eq_add_numeral_1]@add_ac))
-                 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac@add_ac))
+                 THEN ALLGOALS (simp_tac
+				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
   val numeral_simp_tac	= ALLGOALS
                 (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
   end;
@@ -254,9 +255,10 @@
   val prove_conv	= prove_conv "nat_combine_numerals"
   val subst_tac          = subst_tac
   val norm_tac = ALLGOALS
-                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@bin_simps@
+                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
                                        [add_0, Suc_eq_add_numeral_1]@add_ac))
-                 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac@add_ac))
+                 THEN ALLGOALS (simp_tac
+				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
   val numeral_simp_tac	= ALLGOALS
                 (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
   end;
@@ -360,8 +362,6 @@
                                           addsimprocs simprocs
 end;
 
-Delsimprocs [Nat_Plus_Assoc.conv];  (*combine_numerals makes it redundant*)
-
 
 
 (** For simplifying  Suc m - #n **)