author haftmann Thu, 09 Oct 2008 08:47:26 +0200 changeset 28536 8dccb6035d0f parent 28535 38fb0780b58b child 28537 1e84256d1a8a
established canonical argument order
--- 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
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Oct 09 08:47:25 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Oct 09 08:47:26 2008 +0200
@@ -597,7 +597,7 @@
|> Sign.parent_path
-    |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
+    |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
pat_rews @ dist_les @ dist_eqs @ copy_rews)
end; (* let *)

@@ -972,7 +972,7 @@
("finite_ind", [finite_ind]),
("ind"       , [ind       ]),
("coind"     , [coind     ])])))
-       |> Sign.parent_path |> rpair take_rews
+       |> Sign.parent_path |> pair take_rews
end; (* let *)
end; (* local *)
end; (* struct *)