# HG changeset patch
# User haftmann
# Date 1324973726 -3600
# Node ID 15d14fa805b219f475f548c1c6871c6456d76994
# Parent  3289ac99d714bdc9fa1d6e602ed1fb910b14a5f5
prefer canonical fold on lists

diff -r 3289ac99d714 -r 15d14fa805b2 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Dec 27 09:15:26 2011 +0100
+++ b/src/HOL/GCD.thy	Tue Dec 27 09:15:26 2011 +0100
@@ -1486,7 +1486,7 @@
 begin
 
 definition
-  "Lcm (M::nat set) = (if finite M then fold lcm 1 M else 0)"
+  "Lcm (M::nat set) = (if finite M then Finite_Set.fold lcm 1 M else 0)"
 
 definition
   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
@@ -1608,11 +1608,11 @@
 done
 
 lemma Lcm_set_nat [code_unfold]:
-  "Lcm (set ns) = foldl lcm (1::nat) ns"
+  "Lcm (set ns) = fold lcm ns (1::nat)"
   by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
 
 lemma Gcd_set_nat [code_unfold]:
-  "Gcd (set ns) = foldl gcd (0::nat) ns"
+  "Gcd (set ns) = fold gcd ns (0::nat)"
   by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
 
 lemma mult_inj_if_coprime_nat: