fixed theory deps;

--- a/src/HOL/Lex/AutoChopper1.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/AutoChopper1.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -17,7 +17,7 @@
 No proofs yet.
 *)
 
-AutoChopper1 = DA + Chopper + Main +
+AutoChopper1 = DA + Chopper +
 
 consts
   acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)

--- a/src/HOL/Lex/AutoProj.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/AutoProj.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -9,7 +9,7 @@
 and use foldl instead of foldl2.
 *)
 
-AutoProj = Prod +
+AutoProj = Main +
 
 constdefs
  start :: "'a * 'b * 'c => 'a"

--- a/src/HOL/Lex/DA.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/DA.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -6,7 +6,7 @@
 Deterministic automata
 *)
 
-DA = List + AutoProj +
+DA = AutoProj +
 
 types ('a,'s)da = "'s * ('a => 's => 's) * ('s => bool)"
 

--- a/src/HOL/Lex/MaxChop.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/MaxChop.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -4,7 +4,7 @@
     Copyright   1998 TUM
 *)
 
-MaxChop = MaxPrefix + Recdef +
+MaxChop = MaxPrefix +
 
 types   'a chopper = "'a list => 'a list list * 'a list"
 

--- a/src/HOL/Lex/NA.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/NA.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -6,7 +6,7 @@
 Nondeterministic automata
 *)
 
-NA = List + AutoProj +
+NA = AutoProj +
 
 types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
 

--- a/src/HOL/Lex/NAe.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/NAe.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -6,7 +6,7 @@
 Nondeterministic automata with epsilon transitions
 *)
 
-NAe = List + Option + NA +
+NAe = NA +
 
 types ('a,'s)nae = ('a option,'s)na
 

--- a/src/HOL/Lex/ROOT.ML	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/ROOT.ML	Tue Apr 18 00:36:02 2000 +0200
@@ -7,11 +7,5 @@
 use_thy"AutoChopper";
 use_thy"AutoChopper1";
 use_thy"AutoMaxChop";
-(* Do not swap the next two use_thy's.
-   There is some interference, probably via claset() or simpset().
-   Or via ML-bound names of axioms that are overwritten?
-*)
 use_thy"RegSet_of_nat_DA";
-use_thy"RegExp2NA";
-use_thy"RegExp2NAe";
 use_thy"Scanner";

--- a/src/HOL/Lex/RegExp2NA.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/RegExp2NA.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -7,7 +7,7 @@
 into nondeterministic automata *without* epsilon transitions
 *)
 
-RegExp2NA = NA + RegExp +
+RegExp2NA = RegExp + NA +
 
 types 'a bitsNA = ('a,bool list)na
 

--- a/src/HOL/Lex/RegExp2NAe.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/RegExp2NAe.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -7,7 +7,7 @@
 into nondeterministic automata with epsilon transitions
 *)
 
-RegExp2NAe = NAe + RegExp +
+RegExp2NAe = RegExp + NAe +
 
 types 'a bitsNAe = ('a,bool list)nae
 

--- a/src/HOL/Lex/RegSet.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/RegSet.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -6,7 +6,7 @@
 Regular sets
 *)
 
-RegSet = List +
+RegSet = Main +
 
 constdefs
  conc :: 'a list set => 'a list set => 'a list set