src/HOL/Nominal/nominal_package.ML

     val ps = map (fn (_, n, _, _) =>
       (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
     val rps = map Library.swap ps;
 
     fun replace_types (Type ("nominal.ABS", [T, U])) = 
-          Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
+          Type ("fun", [T, Type ("nominal.noption", [replace_types U])])
       | replace_types (Type (s, Ts)) =
           Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
       | replace_types T = T;
 
     fun replace_types' (Type (s, Ts)) =

 
     val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names
       (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
     val big_rep_name =
       space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
-        (fn (i, ("nominal.nOption", _, _)) => NONE
+        (fn (i, ("nominal.noption", _, _)) => NONE
           | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
     val _ = warning ("big_rep_name: " ^ big_rep_name);
 
     fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
           (case AList.lookup op = descr i of
-             SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
+             SOME ("nominal.noption", _, [(_, [dt']), _]) =>
                apfst (cons dt) (strip_option dt')
            | _ => ([], dtf))
-      | strip_option (DtType ("fun", [dt, DtType ("nominal.nOption", [dt'])])) =
+      | strip_option (DtType ("fun", [dt, DtType ("nominal.noption", [dt'])])) =
           apfst (cons dt) (strip_option dt')
       | strip_option dt = ([], dt);
 
     val dt_atomTs = distinct (map (typ_of_dtyp descr sorts')
       (List.concat (map (fn (_, (_, _, cs)) => List.concat

             val free = mk_Free "x" (Us ---> T) j;
             val free' = app_bnds free (length Us);
             fun mk_abs_fun (T, (i, t)) =
               let val U = fastype_of t
               in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
-                Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
+                Type ("nominal.noption", [U])) $ mk_Free "y" T i $ t)
               end
           in (j + 1, j' + length Ts,
             case dt'' of
                 DtRec k => list_all (map (pair "x") Us,
                   HOLogic.mk_Trueprop (HOLogic.mk_mem (free',

       in Logic.list_implies (prems, concl)
       end;
 
     val (intr_ts, ind_consts) =
       apfst List.concat (ListPair.unzip (List.mapPartial
-        (fn ((_, ("nominal.nOption", _, _)), _) => NONE
+        (fn ((_, ("nominal.noption", _, _)), _) => NONE
           | ((i, (_, _, constrs)), rep_set_name) =>
               let val T = nth_dtyp i
               in SOME (map (make_intr rep_set_name T) constrs,
                 Const (rep_set_name, HOLogic.mk_setT T))
               end)

     (**** Prove that representing set is closed under permutation ****)
 
     val _ = warning "proving closure under permutation...";
 
     val perm_indnames' = List.mapPartial
-      (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
+      (fn (x, (_, ("nominal.noption", _, _))) => NONE | (x, _) => SOME x)
       (perm_indnames ~~ descr);
 
     fun mk_perm_closed name = map (fn th => standard (th RS mp))
       (List.take (split_conj_thm (Goal.prove thy4 [] []
         (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map

       let
         val T = fastype_of x;
         val U = fastype_of t
       in
         Const ("nominal.abs_fun", T --> U --> T -->
-          Type ("nominal.nOption", [U])) $ x $ t
+          Type ("nominal.noption", [U])) $ x $ t
       end;
 
     val (ty_idxs, _) = foldl
-      (fn ((i, ("nominal.nOption", _, _)), p) => p
+      (fn ((i, ("nominal.noption", _, _)), p) => p
         | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
 
     fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
       | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
       | reindex dt = dt;

     fun strip_nth_name i s = 
       let val xs = NameSpace.unpack s; 
       in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
 
     val (descr'', ndescr) = ListPair.unzip (List.mapPartial
-      (fn (i, ("nominal.nOption", _, _)) => NONE
+      (fn (i, ("nominal.noption", _, _)) => NONE
         | (i, (s, dts, constrs)) =>
              let
                val SOME index = AList.lookup op = ty_idxs i;
                val (constrs1, constrs2) = ListPair.unzip
                  (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 cname))

       Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
     val abs_names = map (fn s =>
       Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
 
     val recTs' = List.mapPartial
-      (fn ((_, ("nominal.nOption", _, _)), T) => NONE
+      (fn ((_, ("nominal.noption", _, _)), T) => NONE
         | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
     val recTs = get_rec_types descr'' sorts';
     val newTs' = Library.take (length new_type_names, recTs');
     val newTs = Library.take (length new_type_names, recTs);