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