src/Tools/Code/code_thingol.ML
changeset 33420 17b7095ad463
parent 33187 616be6d7997e
child 33943 f31d645b4e00
child 33955 fff6f11b1f09
child 33990 febc68c02b63
--- 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"