special treatment of ==> and == solely as constants
authorhaftmann
Mon Jan 06 09:31:19 2014 +0100 (2014-01-06 ago)
changeset 54932409de8cf33b2
parent 54931 88cf06038e37
child 54933 45624a38109f
special treatment of ==> and == solely as constants
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Jan 06 09:31:18 2014 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Jan 06 09:31:19 2014 +0100
     1.3 @@ -277,13 +277,10 @@
     1.4      | NONE => (case Code.get_type_of_constr_or_abstr thy c
     1.5         of SOME (tyco, _) => thyname_of_type thy tyco
     1.6          | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
     1.7 -  fun purify_base "==>" = "follows"
     1.8 -    | purify_base "==" = "meta_eq"
     1.9 -    | purify_base s = Name.desymbolize false s;
    1.10    fun namify thy get_basename get_thyname name =
    1.11      let
    1.12        val prefix = get_thyname thy name;
    1.13 -      val base = (purify_base o get_basename) name;
    1.14 +      val base = (Name.desymbolize false o get_basename) name;
    1.15      in Long_Name.append prefix base end;
    1.16  in
    1.17  
    1.18 @@ -296,7 +293,9 @@
    1.19    | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_type tyco;
    1.20  fun namify_instance thy = namify thy (fn (class, tyco) => 
    1.21    Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
    1.22 -fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;
    1.23 +fun namify_const thy "==>" = "Pure.follows"
    1.24 +  | namify_const thy "==" = "Pure.meta_eq"
    1.25 +  | namify_const thy c = namify thy Long_Name.base_name thyname_of_const c;
    1.26  
    1.27  end; (* local *)
    1.28