--- a/src/HOLCF/Tools/domain/domain_extender.ML Thu Oct 09 08:47:25 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Thu Oct 09 08:47:26 2008 +0200
@@ -128,9 +128,9 @@
) : cons;
val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
- val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
- Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
- |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
+ val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn eq =>
+ Domain_Theorems.theorems (eq, eqs)) eqs
+ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
|> Sign.add_path (Sign.base_name comp_dnam)