src/HOL/Datatype.thy
changeset 55642 63beb38e9258
parent 55417 01fbfb60c33e
     1.1 --- a/src/HOL/Datatype.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -133,7 +133,7 @@
     1.4  
     1.5  lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
     1.6  apply (simp add: Node_def Push_def) 
     1.7 -apply (fast intro!: apfst_conv nat.cases(2)[THEN trans])
     1.8 +apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
     1.9  done
    1.10  
    1.11