src/ZF/Tools/induct_tacs.ML

 structure DatatypeTactics : DATATYPE_TACTICS =
 struct
 
 fun datatype_info_sg sign name =
   (case Symtab.lookup (DatatypesData.get_sg sign, name) of
-    Some info => info
-  | None => error ("Unknown datatype " ^ quote name));
+    SOME info => info
+  | NONE => error ("Unknown datatype " ^ quote name));
 
 
 (*Given a variable, find the inductive set associated it in the assumptions*)
 exception Find_tname of string
 

              (v, #1 (dest_Const (head_of A)))
         | mk_pair _ = raise Match
       val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))
           (#2 (strip_context Bi))
   in case assoc (pairs, var) of
-       None => raise Find_tname ("Cannot determine datatype of " ^ quote var)
-     | Some t => t
+       NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
+     | SOME t => t
   end;
 
 (** generic exhaustion and induction tactic for datatypes
     Differences from HOL:
       (1) no checking if the induction var occurs in premises, since it always