# HG changeset patch
# User steckerm
# Date 1411202663 -7200
# Node ID 4be5ab4452f41b7a1347e83e6bef88fd3bc82975
# Parent  ede6ca6a54eefe5699d3c254028aaf99973e4ca0
Updated fix_name function

diff -r ede6ca6a54ee -r 4be5ab4452f4 src/HOL/Tools/ATP/atp_waldmeister.ML
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:42:08 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Sat Sep 20 10:44:23 2014 +0200
@@ -389,7 +389,7 @@
       (* Use name instead of encoded_name because Waldmeister renames free variables. *)
     else if name = waldmeister_equals then
       (case args of 
-        [_, _] => eq_const @{typ bool}
+        [_, _] => eq_const dummyT
       | _ => raise FailureMessage 
         (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ 
          Int.toString (length args)))
@@ -541,12 +541,20 @@
 fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of
   SOME x => x |
   NONE => NONE
-  
-fun fix_name name = (* fixme *)
-  if String.isPrefix fact_prefix name then 
-    String.extract(name,7,NONE) |> unascii_of |> curry (op ^) "fact_0_"
-  else
-    name
+
+fun fix_name name =
+  let
+    fun drop_digits' xs [] = (xs, [])
+      | drop_digits' xs (c :: cs) = if Char.isDigit c then drop_digits' (c :: xs) cs else
+        (xs, (c :: cs))
+    fun drop_digits xs = drop_digits' [] xs
+  in
+    if String.isPrefix fact_prefix name then 
+      String.extract(name,size fact_prefix,NONE) |> String.explode |> drop_digits ||> tl 
+        ||> String.implode ||> unascii_of |> (fn (x,y) => fact_prefix ^ String.implode x ^ "_" ^ y)
+    else
+      name
+  end
 
 fun skolemization_steps info
   (proof_step as ((waldmeister_name, isabelle_names), _, trm, rule, _)) =