1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 17 14:35:44 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 17 14:37:16 2010 +0200
     1.3 @@ -85,8 +85,7 @@
     1.4  fun sublinear_minimize _ [] p = p
     1.5    | sublinear_minimize test (x :: xs) (seen, result) =
     1.6      case test (xs @ seen) of
     1.7 -      result as {outcome = NONE, proof, used_thm_names, ...}
     1.8 -      : prover_result =>
     1.9 +      result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
    1.10        sublinear_minimize test (filter_used_facts used_thm_names xs)
    1.11                           (filter_used_facts used_thm_names seen, result)
    1.12      | _ => sublinear_minimize test xs (x :: seen, result)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 17 14:35:44 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 17 14:37:16 2010 +0200
     2.3 @@ -279,10 +279,10 @@
     2.4    | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
     2.5    | add_type_constraint _ = I
     2.6  
     2.7 -fun fix_atp_variable_name s =
     2.8 +fun fix_atp_variable_name f s =
     2.9    let
    2.10      fun subscript_name s n = s ^ nat_subscript n
    2.11 -    val s = String.map Char.toLower s
    2.12 +    val s = String.map f s
    2.13    in
    2.14      case space_explode "_" s of
    2.15        [_] => (case take_suffix Char.isDigit (String.explode s) of
    2.16 @@ -349,9 +349,10 @@
    2.17                    SOME b => Var ((b, 0), T)
    2.18                  | NONE =>
    2.19                    if is_tptp_variable a then
    2.20 -                    Var ((fix_atp_variable_name a, 0), T)
    2.21 +                    Var ((fix_atp_variable_name Char.toLower a, 0), T)
    2.22                    else
    2.23 -                    raise Fail ("Unexpected constant: " ^ quote a)
    2.24 +                    (* Skolem constants? *)
    2.25 +                    Var ((fix_atp_variable_name Char.toUpper a, 0), T)
    2.26            in list_comb (t, ts) end
    2.27    in aux (SOME HOLogic.boolT) [] end
    2.28