# HG changeset patch
# User haftmann
# Date 1268662402 -3600
# Node ID 533dd944e29ca70d049a0dcae76c4869323b1d2c
# Parent  5b95a36c154307d317cf74ea1c799fc773cc5100# Parent  2d44d2a1f68ed7f5503c4673c0757ce566c771bf
merged

diff -r 5b95a36c1543 -r 533dd944e29c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Mar 15 13:59:34 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Mar 15 15:13:22 2010 +0100
@@ -1586,8 +1586,8 @@
 
 end
 
-no_notation (in times) times (infixl "*" 70)
-no_notation (in one) Groups.one ("1")
+no_notation times (infixl "*" 70)
+no_notation Groups.one ("1")
 
 locale folding_image_simple = comm_monoid +
   fixes g :: "('b \<Rightarrow> 'a)"
@@ -1742,8 +1742,8 @@
 
 end
 
-notation (in times) times (infixl "*" 70)
-notation (in one) Groups.one ("1")
+notation times (infixl "*" 70)
+notation Groups.one ("1")
 
 
 subsection {* Finite cardinality *}