# HG changeset patch
# User haftmann
# Date 1223534846 -7200
# Node ID 8dccb6035d0f3ba294d2eb38addd01af1a3b2a53
# Parent  38fb0780b58bdb18103d770e31e5c460434227fd
established canonical argument order

diff -r 38fb0780b58b -r 8dccb6035d0f src/HOLCF/Tools/domain/domain_extender.ML
--- 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)
diff -r 38fb0780b58b -r 8dccb6035d0f src/HOLCF/Tools/domain/domain_theorems.ML
--- 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 @@
     |> (snd o PureThy.add_thmss
         [(("match_rews", mat_rews), [Simplifier.simp_add])])
     |> 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 *)