src/Tools/Code/code_symbol.ML
changeset 56810 4ccfe99c160b
parent 56245 84fc7dfa3cd4
child 56811 b66639331db5
equal deleted inserted replaced
56809:b60009672a65 56810:4ccfe99c160b
    86   val base = Name.desymbolize false o Long_Name.base_name;
    86   val base = Name.desymbolize false o Long_Name.base_name;
    87   fun base_rel (x, y) = base y ^ "_" ^ base x;
    87   fun base_rel (x, y) = base y ^ "_" ^ base x;
    88 in
    88 in
    89 
    89 
    90 fun default_base (Constant "") = "value"
    90 fun default_base (Constant "") = "value"
    91   | default_base (Constant @{const_name Pure.imp}) = "follows"
       
    92   | default_base (Constant @{const_name Pure.eq}) = "meta_eq"
       
    93   | default_base (Constant c) = base c
    91   | default_base (Constant c) = base c
    94   | default_base (Type_Constructor tyco) = base tyco
    92   | default_base (Type_Constructor tyco) = base tyco
    95   | default_base (Type_Class class) = base class
    93   | default_base (Type_Class class) = base class
    96   | default_base (Class_Relation classrel) = base_rel classrel
    94   | default_base (Class_Relation classrel) = base_rel classrel
    97   | default_base (Class_Instance inst) = base_rel inst;
    95   | default_base (Class_Instance inst) = base_rel inst;