src/FOLP/simp.ML
changeset 32952 aeb1e44fbc19
parent 32740 9dd0a2f83429
child 32957 675c0c7e6a37
     1.1 --- a/src/FOLP/simp.ML	Thu Oct 15 23:10:35 2009 +0200
     1.2 +++ b/src/FOLP/simp.ML	Thu Oct 15 23:28:10 2009 +0200
     1.3 @@ -432,8 +432,8 @@
     1.4  fun add_asms(ss,thm,a,anet,ats,cs) =
     1.5      let val As = strip_varify(nth_subgoal i thm, a, []);
     1.6          val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
     1.7 -        val new_rws = List.concat(map mk_rew_rules thms);
     1.8 -        val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
     1.9 +        val new_rws = maps mk_rew_rules thms;
    1.10 +        val rwrls = map mk_trans (maps mk_rew_rules thms);
    1.11          val anet' = List.foldr lhs_insert_thm anet rwrls
    1.12      in  if !tracing andalso not(null new_rws)
    1.13          then writeln (cat_lines
    1.14 @@ -589,7 +589,7 @@
    1.15      val T' = Logic.incr_tvar 9 T;
    1.16  in mk_cong_type thy (Const(f,T'),T') end;
    1.17  
    1.18 -fun mk_congs thy = List.concat o map (mk_cong_thy thy);
    1.19 +fun mk_congs thy = maps (mk_cong_thy thy);
    1.20  
    1.21  fun mk_typed_congs thy =
    1.22  let
    1.23 @@ -599,7 +599,7 @@
    1.24        val t = case Sign.const_type thy f of
    1.25                    SOME(_) => Const(f,T) | NONE => Free(f,T)
    1.26      in (t,T) end
    1.27 -in List.concat o map (mk_cong_type thy o readfT) end;
    1.28 +in maps (mk_cong_type thy o readfT) end;
    1.29  
    1.30  end;
    1.31  end;