author | haftmann |
Thu, 01 May 2014 09:30:34 +0200 | |
changeset 56810 | 4ccfe99c160b |
parent 56809 | b60009672a65 |
child 56811 | b66639331db5 |
--- a/src/Tools/Code/code_symbol.ML Thu May 01 09:30:34 2014 +0200 +++ b/src/Tools/Code/code_symbol.ML Thu May 01 09:30:34 2014 +0200 @@ -88,8 +88,6 @@ in fun default_base (Constant "") = "value" - | default_base (Constant @{const_name Pure.imp}) = "follows" - | default_base (Constant @{const_name Pure.eq}) = "meta_eq" | default_base (Constant c) = base c | default_base (Type_Constructor tyco) = base tyco | default_base (Type_Class class) = base class