# 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 *)