src/HOL/List.thy

--- a/src/HOL/List.thy	Fri Dec 04 11:44:57 2009 +0100
+++ b/src/HOL/List.thy	Fri Dec 04 15:20:24 2009 +0100
@@ -366,7 +366,7 @@
       val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
                                         $ NilC;
       val cs = Syntax.const "_case2" $ case1 $ case2
-      val ft = DatatypeCase.case_tr false Datatype.info_of_constr
+      val ft = Datatype_Case.case_tr false Datatype.info_of_constr
                  ctxt [x, cs]
     in lambda x ft end;