1.1 --- a/src/HOL/Finite_Set.thy	Sun Mar 14 19:48:33 2010 -0700
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Mar 15 15:13:07 2010 +0100
     1.3 @@ -1586,8 +1586,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 -no_notation (in times) times (infixl "*" 70)
     1.8 -no_notation (in one) Groups.one ("1")
     1.9 +no_notation times (infixl "*" 70)
    1.10 +no_notation Groups.one ("1")
    1.11  
    1.12  locale folding_image_simple = comm_monoid +
    1.13    fixes g :: "('b \<Rightarrow> 'a)"
    1.14 @@ -1742,8 +1742,8 @@
    1.15  
    1.16  end
    1.17  
    1.18 -notation (in times) times (infixl "*" 70)
    1.19 -notation (in one) Groups.one ("1")
    1.20 +notation times (infixl "*" 70)
    1.21 +notation Groups.one ("1")
    1.22  
    1.23  
    1.24  subsection {* Finite cardinality *}