# HG changeset patch
# User haftmann
# Date 1278319189 -7200
# Node ID 8e44a83df34ae481e911727afaa1f4443495d1b5
# Parent  c6161bee84860f4fabb5ddc0df82eaa25380b574
dropped passed irregular names

diff -r c6161bee8486 -r 8e44a83df34a src/Tools/Code/code_thingol.ML
--- 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