--- a/src/HOL/Metis_Examples/Binary_Tree.thy Tue Nov 15 09:22:19 2011 +0100
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Tue Nov 15 12:39:29 2011 +0100
@@ -264,7 +264,7 @@
"n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
apply (induct t1)
apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
- semiring_norm(111))
+ Suc_eq_plus1)
by (simp add: left_distrib)
declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]]
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Nov 15 09:22:19 2011 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Nov 15 12:39:29 2011 +0100
@@ -107,6 +107,6 @@
by (metis_exhaust null_def)
lemma "(0::nat) + 0 = 0"
-by (metis_exhaust arithmetic_simps(38))
+by (metis_exhaust add_0_left)
end