changeset 33968 | f94fb13ecbb3 |
parent 33640 | 0d82107dc07a |
child 33972 | daf65be6bfe5 |
--- a/src/HOL/List.thy Mon Nov 30 11:42:48 2009 +0100 +++ b/src/HOL/List.thy Mon Nov 30 11:42:49 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;