TFL/tfl.ML

           end
      else
      let val pty as Type (ty_name,_) = type_of p
      in
      case (ty_info ty_name)
-     of None => mk_case_fail("Not a known datatype: "^ty_name)
-      | Some{case_const,constructors} =>
+     of NONE => mk_case_fail("Not a known datatype: "^ty_name)
+      | SOME{case_const,constructors} =>
         let
             val case_const_name = #1(dest_Const case_const)
             val nrows = List.concat (map (expand constructors pty) rows)
             val subproblems = divide(constructors, pty, range_ty, nrows)
             val groups      = map #group subproblems

  *---------------------------------------------------------------------------*)
 
 
 (*For Isabelle, the lhs of a definition must be a constant.*)
 fun mk_const_def sign (Name, Ty, rhs) =
-    Sign.infer_types (Sign.pp sign) sign (K None) (K None) [] false
+    Sign.infer_types (Sign.pp sign) sign (K NONE) (K NONE) [] false
                ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT)
     |> #1;
 
 (*Make all TVars available for instantiation by adding a ? to the front*)
 fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)

 fun alpha_ex_unroll (xlist, tm) =
   let val (qvars,body) = S.strip_exists tm
       val vlist = #2(S.strip_comb (S.rhs body))
       val plist = ListPair.zip (vlist, xlist)
       val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
-                   handle Library.OPTION => sys_error
+                   handle Option => sys_error
                        "TFL fault [alpha_ex_unroll]: no correspondence"
       fun build ex      []   = []
         | build (_$rex) (v::rst) =
            let val ex1 = betapply(rex, v)
            in  ex1 :: build ex1 rst

           end
      else                     (* column 0 is all constructors *)
      let val Type (ty_name,_) = type_of p
      in
      case (ty_info ty_name)
-     of None => fail("Not a known datatype: "^ty_name)
-      | Some{constructors,nchotomy} =>
+     of NONE => fail("Not a known datatype: "^ty_name)
+      | SOME{constructors,nchotomy} =>
         let val thm' = R.ISPEC (tych u) nchotomy
             val disjuncts = S.strip_disj (concl thm')
             val subproblems = divide(constructors, rows)
             val groups      = map #group subproblems
             and new_formals = map #new_formals subproblems