src/HOL/Nominal/nominal_package.ML
changeset 18579 002d371401f5
parent 18381 246807ef6dfb
child 18582 4f4cc426b440
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Jan 04 20:20:25 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Jan 05 12:09:26 2006 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4      val rps = map Library.swap ps;
     1.5  
     1.6      fun replace_types (Type ("nominal.ABS", [T, U])) = 
     1.7 -          Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
     1.8 +          Type ("fun", [T, Type ("nominal.noption", [replace_types U])])
     1.9        | replace_types (Type (s, Ts)) =
    1.10            Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
    1.11        | replace_types T = T;
    1.12 @@ -386,16 +386,16 @@
    1.13        (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
    1.14      val big_rep_name =
    1.15        space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
    1.16 -        (fn (i, ("nominal.nOption", _, _)) => NONE
    1.17 +        (fn (i, ("nominal.noption", _, _)) => NONE
    1.18            | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
    1.19      val _ = warning ("big_rep_name: " ^ big_rep_name);
    1.20  
    1.21      fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
    1.22            (case AList.lookup op = descr i of
    1.23 -             SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
    1.24 +             SOME ("nominal.noption", _, [(_, [dt']), _]) =>
    1.25                 apfst (cons dt) (strip_option dt')
    1.26             | _ => ([], dtf))
    1.27 -      | strip_option (DtType ("fun", [dt, DtType ("nominal.nOption", [dt'])])) =
    1.28 +      | strip_option (DtType ("fun", [dt, DtType ("nominal.noption", [dt'])])) =
    1.29            apfst (cons dt) (strip_option dt')
    1.30        | strip_option dt = ([], dt);
    1.31  
    1.32 @@ -417,7 +417,7 @@
    1.33              fun mk_abs_fun (T, (i, t)) =
    1.34                let val U = fastype_of t
    1.35                in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
    1.36 -                Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
    1.37 +                Type ("nominal.noption", [U])) $ mk_Free "y" T i $ t)
    1.38                end
    1.39            in (j + 1, j' + length Ts,
    1.40              case dt'' of
    1.41 @@ -438,7 +438,7 @@
    1.42  
    1.43      val (intr_ts, ind_consts) =
    1.44        apfst List.concat (ListPair.unzip (List.mapPartial
    1.45 -        (fn ((_, ("nominal.nOption", _, _)), _) => NONE
    1.46 +        (fn ((_, ("nominal.noption", _, _)), _) => NONE
    1.47            | ((i, (_, _, constrs)), rep_set_name) =>
    1.48                let val T = nth_dtyp i
    1.49                in SOME (map (make_intr rep_set_name T) constrs,
    1.50 @@ -456,7 +456,7 @@
    1.51      val _ = warning "proving closure under permutation...";
    1.52  
    1.53      val perm_indnames' = List.mapPartial
    1.54 -      (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
    1.55 +      (fn (x, (_, ("nominal.noption", _, _))) => NONE | (x, _) => SOME x)
    1.56        (perm_indnames ~~ descr);
    1.57  
    1.58      fun mk_perm_closed name = map (fn th => standard (th RS mp))
    1.59 @@ -580,11 +580,11 @@
    1.60          val U = fastype_of t
    1.61        in
    1.62          Const ("nominal.abs_fun", T --> U --> T -->
    1.63 -          Type ("nominal.nOption", [U])) $ x $ t
    1.64 +          Type ("nominal.noption", [U])) $ x $ t
    1.65        end;
    1.66  
    1.67      val (ty_idxs, _) = foldl
    1.68 -      (fn ((i, ("nominal.nOption", _, _)), p) => p
    1.69 +      (fn ((i, ("nominal.noption", _, _)), p) => p
    1.70          | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
    1.71  
    1.72      fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
    1.73 @@ -599,7 +599,7 @@
    1.74        in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    1.75  
    1.76      val (descr'', ndescr) = ListPair.unzip (List.mapPartial
    1.77 -      (fn (i, ("nominal.nOption", _, _)) => NONE
    1.78 +      (fn (i, ("nominal.noption", _, _)) => NONE
    1.79          | (i, (s, dts, constrs)) =>
    1.80               let
    1.81                 val SOME index = AList.lookup op = ty_idxs i;
    1.82 @@ -624,7 +624,7 @@
    1.83        Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
    1.84  
    1.85      val recTs' = List.mapPartial
    1.86 -      (fn ((_, ("nominal.nOption", _, _)), T) => NONE
    1.87 +      (fn ((_, ("nominal.noption", _, _)), T) => NONE
    1.88          | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
    1.89      val recTs = get_rec_types descr'' sorts';
    1.90      val newTs' = Library.take (length new_type_names, recTs');