# HG changeset patch
# User haftmann
# Date 1398929434 -7200
# Node ID 4ccfe99c160b95c21537ea1125b1a407c81209fc
# Parent  b60009672a65e8445b0b2f5b8f0acb5ff4dbed89
obsolete: no symbol identifiers remaining in Pure

diff -r b60009672a65 -r 4ccfe99c160b src/Tools/Code/code_symbol.ML
--- 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