src/HOL/Tools/inductive_codegen.ML
changeset 30190 479806475f3c
parent 29287 5b0bfd63b5da
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4            {intros = intros |>
     1.5             Symtab.update (s, (AList.update Thm.eq_thm_prop
     1.6               (thm, (thyname_of s, nparms)) rules)),
     1.7 -           graph = foldr (uncurry (Graph.add_edge o pair s))
     1.8 +           graph = List.foldr (uncurry (Graph.add_edge o pair s))
     1.9               (Library.foldl add_node (graph, s :: cs)) cs,
    1.10             eqns = eqns} thy
    1.11          end
    1.12 @@ -152,7 +152,7 @@
    1.13  fun cprod ([], ys) = []
    1.14    | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
    1.15  
    1.16 -fun cprods xss = foldr (map op :: o cprod) [[]] xss;
    1.17 +fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
    1.18  
    1.19  datatype mode = Mode of (int list option list * int list) * int list * mode option list;
    1.20  
    1.21 @@ -357,7 +357,7 @@
    1.22  
    1.23      val (in_ts, out_ts) = get_args is 1 ts;
    1.24      val ((all_vs', eqs), in_ts') =
    1.25 -      foldl_map check_constrt ((all_vs, []), in_ts);
    1.26 +      Library.foldl_map check_constrt ((all_vs, []), in_ts);
    1.27  
    1.28      fun compile_prems out_ts' vs names [] gr =
    1.29            let
    1.30 @@ -365,8 +365,8 @@
    1.31                (invoke_codegen thy defs dep module false) out_ts gr;
    1.32              val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
    1.33              val ((names', eqs'), out_ts'') =
    1.34 -              foldl_map check_constrt ((names, []), out_ts');
    1.35 -            val (nvs, out_ts''') = foldl_map distinct_v
    1.36 +              Library.foldl_map check_constrt ((names, []), out_ts');
    1.37 +            val (nvs, out_ts''') = Library.foldl_map distinct_v
    1.38                ((names', map (fn x => (x, [x])) vs), out_ts'');
    1.39              val (out_ps', gr4) = fold_map
    1.40                (invoke_codegen thy defs dep module false) (out_ts''') gr3;
    1.41 @@ -383,8 +383,8 @@
    1.42                select_mode_prem thy modes' vs' ps;
    1.43              val ps' = filter_out (equal p) ps;
    1.44              val ((names', eqs), out_ts') =
    1.45 -              foldl_map check_constrt ((names, []), out_ts);
    1.46 -            val (nvs, out_ts'') = foldl_map distinct_v
    1.47 +              Library.foldl_map check_constrt ((names, []), out_ts);
    1.48 +            val (nvs, out_ts'') = Library.foldl_map distinct_v
    1.49                ((names', map (fn x => (x, [x])) vs), out_ts');
    1.50              val (out_ps, gr0) = fold_map
    1.51                (invoke_codegen thy defs dep module false) out_ts'' gr;