--- 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)
--- 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