dropped passed irregular names

--- a/src/Tools/Code/code_thingol.ML	Sat Jul 03 00:50:35 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Jul 05 10:39:49 2010 +0200
@@ -267,10 +267,7 @@
     | purify_base "op &" = "and"
     | purify_base "op |" = "or"
     | purify_base "op -->" = "implies"
-    | purify_base "op :" = "member"
     | purify_base "op =" = "eq"
-    | purify_base "*" = "product"
-    | purify_base "+" = "sum"
     | purify_base s = Name.desymbolize false s;
   fun namify thy get_basename get_thyname name =
     let