1) have adjusted the swapping of the result type
authorurbanc
Sat Oct 29 14:37:32 2005 +0200 (2005-10-29)
changeset 180456d69a4190eb2
parent 18044 f27022e2ec3a
child 18046 b7389981170b
1) have adjusted the swapping of the result type
in add_datatype_i
2) have replaced map_nth_elem by Library.nth_map
(there seems to be a clash with an existing
nth_map somewhere - therefore the "Library")
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 22:37:57 2005 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Oct 29 14:37:32 2005 +0200
     1.3 @@ -1039,7 +1039,7 @@
     1.4      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
     1.5      val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';
     1.6  
     1.7 -    val (thy1, {induction, ...}) =
     1.8 +    val ({induction, ...},thy1) =
     1.9        DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
    1.10  
    1.11      val SOME {descr, ...} = Symtab.lookup
    1.12 @@ -1498,9 +1498,9 @@
    1.13      fun strip_suffix i s = implode (List.take (explode s, size s - i));
    1.14  
    1.15      (** strips the "_Rep" in type names *)
    1.16 -    fun strip_nth_name i s =
    1.17 -      let val xs = NameSpace.unpack s
    1.18 -      in NameSpace.pack (map_nth_elem (length xs - i) (strip_suffix 4) xs) end;
    1.19 +    fun strip_nth_name i s = 
    1.20 +      let val xs = NameSpace.unpack s; 
    1.21 +      in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    1.22  
    1.23      val descr'' = List.mapPartial
    1.24        (fn (i, ("nominal.nOption", _, _)) => NONE
    1.25 @@ -1511,6 +1511,7 @@
    1.26                  foldl (fn (dt, dts) =>
    1.27                    let val (dts', dt') = strip_option dt
    1.28                    in (dts @ dts' @ [reindex dt']) end) [] cargs)) constrs))) descr;
    1.29 +
    1.30      val (descr1, descr2) = splitAt (length new_type_names, descr'');
    1.31      val descr' = [descr1, descr2];
    1.32