# HG changeset patch
# User haftmann
# Date 1388997079 -3600
# Node ID 409de8cf33b2b8cb9de3ff8c16f6561f920de20b
# Parent  88cf06038e37dc93c43dbb4ad1bf1caeea587e2c
special treatment of ==> and == solely as constants

diff -r 88cf06038e37 -r 409de8cf33b2 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Jan 06 09:31:18 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Jan 06 09:31:19 2014 +0100
@@ -277,13 +277,10 @@
     | NONE => (case Code.get_type_of_constr_or_abstr thy c
        of SOME (tyco, _) => thyname_of_type thy tyco
         | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
-  fun purify_base "==>" = "follows"
-    | purify_base "==" = "meta_eq"
-    | purify_base s = Name.desymbolize false s;
   fun namify thy get_basename get_thyname name =
     let
       val prefix = get_thyname thy name;
-      val base = (purify_base o get_basename) name;
+      val base = (Name.desymbolize false o get_basename) name;
     in Long_Name.append prefix base end;
 in
 
@@ -296,7 +293,9 @@
   | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_type tyco;
 fun namify_instance thy = namify thy (fn (class, tyco) => 
   Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
-fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;
+fun namify_const thy "==>" = "Pure.follows"
+  | namify_const thy "==" = "Pure.meta_eq"
+  | namify_const thy c = namify thy Long_Name.base_name thyname_of_const c;
 
 end; (* local *)