src/HOL/List.thy

--- a/src/HOL/List.thy	Thu Jun 18 18:31:14 2009 -0700
+++ b/src/HOL/List.thy	Fri Jun 19 17:23:21 2009 +0200
@@ -363,7 +363,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 DatatypePackage.datatype_of_constr
+      val ft = DatatypeCase.case_tr false Datatype.datatype_of_constr
                  ctxt [x, cs]
     in lambda x ft end;