src/Pure/Proof/extraction.ML
changeset 33337 9c3b9bf81e8b
parent 33317 b4534348b8fd
child 33388 d64545e6cba5
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Oct 29 20:53:24 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Oct 29 23:48:56 2009 +0100
     1.3 @@ -77,12 +77,12 @@
     1.4  
     1.5  val empty_rules : rules = {next = 0, rs = [], net = Net.empty};
     1.6  
     1.7 -fun add_rule (r as (_, (lhs, _)), {next, rs, net} : rules) =
     1.8 +fun add_rule (r as (_, (lhs, _))) ({next, rs, net} : rules) =
     1.9    {next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
    1.10       (Envir.eta_contract lhs, (next, r)) net};
    1.11  
    1.12  fun merge_rules ({next, rs = rs1, net} : rules) ({rs = rs2, ...} : rules) =
    1.13 -  List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
    1.14 +  fold_rev add_rule (subtract (op =) rs1 rs2) {next = next, rs = rs1, net = net};
    1.15  
    1.16  fun condrew thy rules procs =
    1.17    let
    1.18 @@ -231,7 +231,7 @@
    1.19      defs, expand, prep} = ExtractionData.get thy;
    1.20    in
    1.21      ExtractionData.put
    1.22 -      {realizes_eqns = List.foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
    1.23 +      {realizes_eqns = fold_rev add_rule (map (prep_eq thy) eqns) realizes_eqns,
    1.24         typeof_eqns = typeof_eqns, types = types, realizers = realizers,
    1.25         defs = defs, expand = expand, prep = prep} thy
    1.26    end
    1.27 @@ -249,7 +249,7 @@
    1.28    in
    1.29      ExtractionData.put
    1.30        {realizes_eqns = realizes_eqns, realizers = realizers,
    1.31 -       typeof_eqns = List.foldr add_rule typeof_eqns eqns',
    1.32 +       typeof_eqns = fold_rev add_rule eqns' typeof_eqns,
    1.33         types = types, defs = defs, expand = expand, prep = prep} thy
    1.34    end
    1.35  
    1.36 @@ -359,8 +359,8 @@
    1.37    in
    1.38      (ExtractionData.put (if is_def then
    1.39          {realizes_eqns = realizes_eqns,
    1.40 -         typeof_eqns = add_rule (([],
    1.41 -           Logic.dest_equals (prop_of (Drule.abs_def thm))), typeof_eqns),
    1.42 +         typeof_eqns = add_rule ([],
    1.43 +           Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
    1.44           types = types,
    1.45           realizers = realizers, defs = insert Thm.eq_thm thm defs,
    1.46           expand = expand, prep = prep}
    1.47 @@ -458,7 +458,7 @@
    1.48          val vars = vars_of prop;
    1.49          val n = Int.min (length vars, length ts);
    1.50  
    1.51 -        fun add_args ((Var ((a, i), _), t), (vs', tye)) =
    1.52 +        fun add_args (Var ((a, i), _), t) (vs', tye) =
    1.53            if member (op =) rvs a then
    1.54              let val T = etype_of thy' vs Ts t
    1.55              in if T = nullT then (vs', tye)
    1.56 @@ -466,7 +466,7 @@
    1.57              end
    1.58            else (vs', tye)
    1.59  
    1.60 -      in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    1.61 +      in fold_rev add_args (Library.take (n, vars) ~~ Library.take (n, ts)) ([], []) end;
    1.62  
    1.63      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
    1.64      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);