# HG changeset patch
# User blanchet
# Date 1282048636 -7200
# Node ID 3abda3c76df94a68fb74e857d6c49d17fc2607c1
# Parent  1b460d6a9d583e0f9ce2d94e74102b2903dbae73
handle E's Skolem constants more gracefully

diff -r 1b460d6a9d58 -r 3abda3c76df9 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 17 14:35:44 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 17 14:37:16 2010 +0200
@@ -85,8 +85,7 @@
 fun sublinear_minimize _ [] p = p
   | sublinear_minimize test (x :: xs) (seen, result) =
     case test (xs @ seen) of
-      result as {outcome = NONE, proof, used_thm_names, ...}
-      : prover_result =>
+      result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
       sublinear_minimize test (filter_used_facts used_thm_names xs)
                          (filter_used_facts used_thm_names seen, result)
     | _ => sublinear_minimize test xs (x :: seen, result)
diff -r 1b460d6a9d58 -r 3abda3c76df9 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 17 14:35:44 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 17 14:37:16 2010 +0200
@@ -279,10 +279,10 @@
   | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   | add_type_constraint _ = I
 
-fun fix_atp_variable_name s =
+fun fix_atp_variable_name f s =
   let
     fun subscript_name s n = s ^ nat_subscript n
-    val s = String.map Char.toLower s
+    val s = String.map f s
   in
     case space_explode "_" s of
       [_] => (case take_suffix Char.isDigit (String.explode s) of
@@ -349,9 +349,10 @@
                   SOME b => Var ((b, 0), T)
                 | NONE =>
                   if is_tptp_variable a then
-                    Var ((fix_atp_variable_name a, 0), T)
+                    Var ((fix_atp_variable_name Char.toLower a, 0), T)
                   else
-                    raise Fail ("Unexpected constant: " ^ quote a)
+                    (* Skolem constants? *)
+                    Var ((fix_atp_variable_name Char.toUpper a, 0), T)
           in list_comb (t, ts) end
   in aux (SOME HOLogic.boolT) [] end