diff -r 0b9eb4b0ad98 -r 778507520684 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Tue Mar 07 14:09:48 2006 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Tue Mar 07 16:03:31 2006 +0100
@@ -30,7 +30,8 @@
   DEF_NUM_REP
   TYDEF_sum
   DEF_INL
-  DEF_INR;
+  DEF_INR
+  TYDEF_option;
 
 type_maps
   ind > Nat.ind
@@ -39,7 +40,8 @@
   N_1 >  Product_Type.unit
   prod > "*"
   num > nat
-  sum > "+";
+  sum > "+"
+  option > Datatype.option;
 
 const_renames
   "==" > "eqeq"