src/HOL/Tools/datatype_package.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15661 9ef583b08647
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4  fun occs_in_prems tacf vars =
     1.5    SUBGOAL (fn (Bi, i) =>
     1.6             (if  exists (fn Free (a, _) => a mem vars)
     1.7 -                      (Library.foldr add_term_frees (#2 (strip_context Bi), []))
     1.8 +                      (foldr add_term_frees [] (#2 (strip_context Bi)))
     1.9               then warning "Induction variable occurs also among premises!"
    1.10               else ();
    1.11              tacf i));
    1.12 @@ -431,7 +431,7 @@
    1.13                   if length dt <> length vs then
    1.14                      case_error ("Wrong number of arguments for constructor " ^ s)
    1.15                        (SOME tname) vs
    1.16 -                 else (cases \ c, Library.foldr abstr (vs, t)))
    1.17 +                 else (cases \ c, foldr abstr t vs))
    1.18            val (cases'', fs) = foldl_map find_case (cases', constrs)
    1.19          in case (cases'', length constrs = length cases', default) of
    1.20              ([], true, SOME _) =>
    1.21 @@ -542,32 +542,32 @@
    1.22  (********************* axiomatic introduction of datatypes ********************)
    1.23  
    1.24  fun add_and_get_axioms_atts label tnames attss ts thy =
    1.25 -  Library.foldr (fn (((tname, atts), t), (thy', axs)) =>
    1.26 +  foldr (fn (((tname, atts), t), (thy', axs)) =>
    1.27      let
    1.28        val (thy'', [ax]) = thy' |>
    1.29          Theory.add_path tname |>
    1.30          PureThy.add_axioms_i [((label, t), atts)];
    1.31      in (Theory.parent_path thy'', ax::axs)
    1.32 -    end) (tnames ~~ attss ~~ ts, (thy, []));
    1.33 +    end) (thy, []) (tnames ~~ attss ~~ ts);
    1.34  
    1.35  fun add_and_get_axioms label tnames =
    1.36    add_and_get_axioms_atts label tnames (replicate (length tnames) []);
    1.37  
    1.38  fun add_and_get_axiomss label tnames tss thy =
    1.39 -  Library.foldr (fn ((tname, ts), (thy', axss)) =>
    1.40 +  foldr (fn ((tname, ts), (thy', axss)) =>
    1.41      let
    1.42        val (thy'', [axs]) = thy' |>
    1.43          Theory.add_path tname |>
    1.44          PureThy.add_axiomss_i [((label, ts), [])];
    1.45      in (Theory.parent_path thy'', axs::axss)
    1.46 -    end) (tnames ~~ tss, (thy, []));
    1.47 +    end) (thy, []) (tnames ~~ tss);
    1.48  
    1.49  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    1.50      case_names_induct case_names_exhausts thy =
    1.51    let
    1.52      val descr' = List.concat descr;
    1.53      val recTs = get_rec_types descr' sorts;
    1.54 -    val used = Library.foldr add_typ_tfree_names (recTs, []);
    1.55 +    val used = foldr add_typ_tfree_names [] recTs;
    1.56      val newTs = Library.take (length (hd descr), recTs);
    1.57  
    1.58      val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
    1.59 @@ -694,7 +694,7 @@
    1.60        Theory.add_path (space_implode "_" new_type_names) |>
    1.61        add_rules simps case_thms size_thms rec_thms inject distinct
    1.62                  weak_case_congs Simplifier.cong_add_global |> 
    1.63 -      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
    1.64 +      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
    1.65        add_cases_induct dt_infos induct |>
    1.66        Theory.parent_path |>
    1.67        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.68 @@ -752,7 +752,7 @@
    1.69        Theory.add_path (space_implode "_" new_type_names) |>
    1.70        add_rules simps case_thms size_thms rec_thms inject distinct
    1.71                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    1.72 -      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
    1.73 +      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
    1.74        add_cases_induct dt_infos induct |>
    1.75        Theory.parent_path |>
    1.76        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.77 @@ -860,7 +860,7 @@
    1.78        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    1.79        add_rules simps case_thms size_thms rec_thms inject distinct
    1.80                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    1.81 -      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
    1.82 +      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
    1.83        add_cases_induct dt_infos induction' |>
    1.84        Theory.parent_path |>
    1.85        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.86 @@ -916,7 +916,7 @@
    1.87          fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
    1.88            let
    1.89              val (cargs', sorts'') = Library.foldl (prep_typ sign) (([], sorts'), cargs);
    1.90 -            val _ = (case Library.foldr add_typ_tfree_names (cargs', []) \\ tvs of
    1.91 +            val _ = (case foldr add_typ_tfree_names [] cargs' \\ tvs of
    1.92                  [] => ()
    1.93                | vs => error ("Extra type variables on rhs: " ^ commas vs))
    1.94            in (constrs @ [((if flat_names then Sign.full_name sign else