# HG changeset patch
# User haftmann
# Date 1268662387 -3600
# Node ID 2d44d2a1f68ed7f5503c4673c0757ce566c771bf
# Parent  8cd7134275cc3cbfc046a5fbc1b930aa2ed726c3
corrected disastrous syntax declarations

diff -r 8cd7134275cc -r 2d44d2a1f68e src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Mar 14 19:48:33 2010 -0700
+++ b/src/HOL/Finite_Set.thy	Mon Mar 15 15:13:07 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 *}