# HG changeset patch
# User sultana
# Date 1334675647 -3600
# Node ID 0a870584145fee8b58cfa1f2025875e080c6792c
# Parent  50a424b8995253af601a760a5eed1c8fcda8e6d7
improved handling of quoted names in tptp import

diff -r 50a424b89952 -r 0a870584145f 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
@@ -187,10 +187,25 @@
 
 val IND_TYPE = "ind"
 
+(*transform quoted names into acceptable ASCII strings*)
+fun alphanumerate c =
+  let
+    val c' = ord c
+    val out_of_range =
+      ((c' > 64) andalso (c' < 91)) orelse ((c' > 96)
+       andalso (c' < 123)) orelse ((c' > 47) andalso (c' < 58))
+  in
+    if (not out_of_range) andalso (not (c = "_")) then
+      "_nom_" ^ Int.toString (ord c) ^ "_"
+    else c
+  end
+fun alphanumerated_name prefix name =
+  prefix ^ (raw_explode #> map alphanumerate #> implode) name
+
 (*SMLNJ complains if type annotation not used below*)
 fun mk_binding (config : config) ident =
   let
-    val pre_binding = Binding.name ident
+    val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)
   in
     case #problem_name config of
       NONE => pre_binding
@@ -523,22 +538,8 @@
           else dummy_term () (*FIXME: not yet supporting rationals and reals*)
       in (num_term, thy) end
   | Term_Distinct_Object str =>
-      let
-        fun alphanumerate c =
-          let
-            val c' = ord c
-            val out_of_range =
-              ((c' > 64) andalso (c' < 91)) orelse ((c' > 96)
-               andalso (c' < 123)) orelse ((c' > 47) andalso (c' < 58))
-          in
-            if (not out_of_range) andalso (not (c = "_")) then
-              "_nom_" ^ Int.toString (ord c) ^ "_"
-            else c
-          end
-        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
+      declare_constant config (alphanumerated_name "ds_" str)
+        (interpret_type config thy type_map (Defined_type Type_Ind)) thy
 
 (*Given a list of "'a option", then applies a function to each element if that
 element is SOME value, otherwise it leaves it as NONE.*)