--- a/src/HOL/ex/Fundefs.thy Mon Jul 16 19:18:23 2007 +0200 +++ b/src/HOL/ex/Fundefs.thy Mon Jul 16 21:16:16 2007 +0200 @@ -169,7 +169,7 @@ thm evn.simps thm od.simps -thm evn_od.pinduct +thm evn_od.induct thm evn_od.termination