Function 'step' is already defined in NA.thy.

--- a/src/HOL/Lex/NAe.thy	Tue Sep 15 10:40:40 1998 +0200
+++ b/src/HOL/Lex/NAe.thy	Tue Sep 15 13:09:23 1998 +0200
@@ -10,10 +10,6 @@
 
 types ('a,'s)nae = ('a option,'s)na
 
-constdefs
- step :: "('a,'s)nae => 'a option => ('s * 's)set"
-"step A a == {(p,q) . q : next A a p}"
-
 syntax eps :: "('a,'s)nae => ('s * 's)set"
 translations "eps A" == "step A None"