# HG changeset patch
# User sultana
# Date 1334675647 -3600
# Node ID 50a424b8995253af601a760a5eed1c8fcda8e6d7
# Parent  b381d428a7259dfd88bc19ef2ebc66b8d6b67fcf
improved naming of 'distinct objects' in tptp import

diff -r b381d428a725 -r 50a424b89952 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
@@ -535,8 +535,8 @@
               "_nom_" ^ Int.toString (ord c) ^ "_"
             else c
           end
-        val mangle_name = raw_explode #> map alphanumerate #> implode
-      in declare_constant config (mangle_name str)
+        val alphanumerated_name = raw_explode #> map alphanumerate #> implode
+      in declare_constant config ("ds_" ^ alphanumerated_name str)
           (interpret_type config thy type_map (Defined_type Type_Ind)) thy
       end
 
@@ -745,7 +745,7 @@
                          []),
                         thy')
                     end
-  
+
                | _ => (*declaration of constant*)
                   (*Here we populate the map from constants to the Isabelle/HOL
                   terms they map to (which in turn contain their types).*)
@@ -788,7 +788,7 @@
                       thy')(*theory was extended with new constant*)
                   end
              end
-  
+
          | _ => (*i.e. the AF is not a type declaration*)
              let
                (*gather interpreted term, and the map of types occurring in that term*)