# HG changeset patch
# User haftmann
# Date 1257264368 -3600
# Node ID 17b7095ad4631016033b24d6868b6a042c9ad2fb
# Parent  d9a25a87da4a226c1531daa79857bc5f220a8543
pretty name for ==>

diff -r d9a25a87da4a -r 17b7095ad463 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Nov 02 18:49:53 2009 -0800
+++ b/src/Tools/Code/code_thingol.ML	Tue Nov 03 17:06:08 2009 +0100
@@ -261,7 +261,8 @@
     | NONE => (case Code.get_datatype_of_constr thy c
        of SOME dtco => Codegen.thyname_of_type thy dtco
         | NONE => Codegen.thyname_of_const thy c);
-  fun purify_base "op &" = "and"
+  fun purify_base "==>" = "follows"
+    | purify_base "op &" = "and"
     | purify_base "op |" = "or"
     | purify_base "op -->" = "implies"
     | purify_base "op :" = "member"