1.1 --- a/src/HOL/GCD.thy	Tue Dec 27 09:15:26 2011 +0100
     1.2 +++ b/src/HOL/GCD.thy	Tue Dec 27 09:15:26 2011 +0100
     1.3 @@ -1486,7 +1486,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "Lcm (M::nat set) = (if finite M then fold lcm 1 M else 0)"
     1.8 +  "Lcm (M::nat set) = (if finite M then Finite_Set.fold lcm 1 M else 0)"
     1.9  
    1.10  definition
    1.11    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
    1.12 @@ -1608,11 +1608,11 @@
    1.13  done
    1.14  
    1.15  lemma Lcm_set_nat [code_unfold]:
    1.16 -  "Lcm (set ns) = foldl lcm (1::nat) ns"
    1.17 +  "Lcm (set ns) = fold lcm ns (1::nat)"
    1.18    by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
    1.19  
    1.20  lemma Gcd_set_nat [code_unfold]:
    1.21 -  "Gcd (set ns) = foldl gcd (0::nat) ns"
    1.22 +  "Gcd (set ns) = fold gcd ns (0::nat)"
    1.23    by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
    1.24  
    1.25  lemma mult_inj_if_coprime_nat: