src/HOL/Metis_Examples/BT.thy

--- a/src/HOL/Metis_Examples/BT.thy	Thu May 06 23:37:07 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy	Fri May 07 09:59:24 2010 +0200
@@ -88,7 +88,7 @@
   case Lf thus ?case by (metis reflect.simps(1))
 next
   case (Br a t1 t2) thus ?case
-    by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
+    by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
 qed
 
 declare [[ atp_problem_prefix = "BT__depth_reflect" ]]