--- a/src/Tools/Code/code_thingol.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Aug 27 10:56:46 2010 +0200
@@ -271,9 +271,6 @@
of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
| NONE => Codegen.thyname_of_const thy c);
fun purify_base "==>" = "follows"
- | purify_base "op &" = "and"
- | purify_base "op |" = "or"
- | purify_base "op -->" = "implies"
| purify_base "op =" = "eq"
| purify_base s = Name.desymbolize false s;
fun namify thy get_basename get_thyname name =