--- a/src/HOL/Tools/numeral_simprocs.ML Thu Dec 02 15:37:32 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Thu Dec 02 16:04:22 2010 +0100
@@ -764,7 +764,7 @@
(*examples:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s, by (Simp_tac 1));
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
@@ -803,7 +803,7 @@
(*examples:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Simp_tac 1));
test "9*x = 12 * (y::int)";
@@ -873,7 +873,7 @@
(*examples:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Asm_simp_tac 1));
test "x*k = k*(y::int)";
@@ -890,7 +890,7 @@
(*And the same examples for fields such as rat or real:
print_depth 22;
set timing;
-set trace_simp;
+set simp_trace;
fun test s = (Goal s; by (Asm_simp_tac 1));
test "x*k = k*(y::rat)";