# HG changeset patch
# User paulson
# Date 1122566062 -7200
# Node ID f025e0dc638bfaf2e5667efbdc19ba21223990de
# Parent  9ce755a0d61345c2a047840fa4086d637ad7b9da
uniform treatment of variable prefixes

diff -r 9ce755a0d613 -r f025e0dc638b src/HOL/Tools/ATP/recon_parse.ML
--- a/src/HOL/Tools/ATP/recon_parse.ML	Thu Jul 28 16:59:30 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML	Thu Jul 28 17:54:22 2005 +0200
@@ -366,28 +366,26 @@
 
 (* FIX - should change the stars and pluses to many rather than explicit patterns *)
 
+fun trim_prefix a b =
+  let val n = String.size a 
+  in  String.substring (b, n, (size b) - n)  end;
+  
+
 (* FIX - add the other things later *)
-fun remove_typeinfo x  =  if (String.isPrefix "v_" x )
-                            then 
-                                 (String.substring (x,2, ((size x) - 2)))
-                            else if (String.isPrefix "V_" x )
-                                 then 
-                                      (String.substring (x,2, ((size x) - 2)))
-                                 else if (String.isPrefix "typ_" x )
-                                      then 
-                                          ""
-                                      else if (String.isPrefix "Typ_" x )
-                                           then 
-                                                ""
-                                           else  if (String.isPrefix "tconst_" x )
-                                                 then 
-                                                      ""
-                                                 else  if (String.isPrefix "const_" x )
-                                                       then 
-                                                            (String.substring  (x,6, ((size x) - 6)))
-                                                       else
-                                                           x
-                                               
+fun remove_typeinfo x  =  
+    if String.isPrefix ResClause.fixed_var_prefix x
+    then trim_prefix ResClause.fixed_var_prefix x
+    else if String.isPrefix ResClause.schematic_var_prefix x
+    then trim_prefix ResClause.schematic_var_prefix x
+    else if String.isPrefix ResClause.const_prefix x
+    then trim_prefix ResClause.const_prefix x
+    else if String.isPrefix ResClause.tfree_prefix x
+    then ""
+    else if String.isPrefix ResClause.tvar_prefix x
+    then ""
+    else if String.isPrefix ResClause.tconst_prefix x
+    then ""
+    else x;                                               
 
 fun term input = (  ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) =>  (a@b))
                   ) input
diff -r 9ce755a0d613 -r f025e0dc638b src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu Jul 28 16:59:30 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Thu Jul 28 17:54:22 2005 +0200
@@ -34,6 +34,15 @@
     val untyped : unit -> unit
     val clause2tptp : clause -> string * string list
     val tfree_clause : string -> string
+    val schematic_var_prefix : string
+    val fixed_var_prefix : string
+    val tvar_prefix : string
+    val tfree_prefix : string
+    val clause_prefix : string 
+    val arclause_prefix : string
+    val const_prefix : string
+    val tconst_prefix : string 
+    val class_prefix : string 
   end;
 
 structure ResClause : RES_CLAUSE =