src/Pure/drule.ML
changeset 2672 85d7e800d754
parent 2266 82aef6857c5b
child 3530 d9ca80f0759c
     1.1 --- a/src/Pure/drule.ML	Fri Feb 21 15:30:41 1997 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Feb 21 15:31:47 1997 +0100
     1.3 @@ -80,10 +80,10 @@
     1.4  (*results may contain duplicates!*)
     1.5  
     1.6  fun ancestry_of thy =
     1.7 -  thy :: flat (map ancestry_of (parents_of thy));
     1.8 +  thy :: List.concat (map ancestry_of (parents_of thy));
     1.9  
    1.10  val all_axioms_of =
    1.11 -  flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
    1.12 +  List.concat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
    1.13  
    1.14  
    1.15  (* clash_types, clash_consts *)
    1.16 @@ -389,7 +389,7 @@
    1.17  fun thas RLN (i,thbs) =
    1.18    let val resolve = biresolution false (map (pair false) thas) i
    1.19        fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => []
    1.20 -  in  flat (map resb thbs)  end;
    1.21 +  in  List.concat (map resb thbs)  end;
    1.22  
    1.23  fun thas RL thbs = thas RLN (1,thbs);
    1.24