src/HOL/Makefile

 
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
         mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
-        Sexp Univ List RelPow
+        Sexp Univ List RelPow Option
 
 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
 	ind_syntax.ML cladata.ML simpdata.ML\
 	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML\
 	../Provers/hypsubst.ML ../Provers/classical.ML\

 
 ##I/O Automata
 IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
                 Receiver Sender
 IOA_ABP_NAMES = Action Correctness Lemmas
-IOA_MT_NAMES = Asig IOA Option Solve
+IOA_MT_NAMES = Asig IOA Solve
 
 IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy\
  $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML)\
  IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy\
  IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy\