tuning
authorblanchet
Tue Aug 17 16:47:40 2010 +0200 (2010-08-17)
changeset 3849057de0f12516f
parent 38489 124193c26751
child 38491 f7e51d981a9f
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 17 16:46:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 17 16:47:40 2010 +0200
     1.3 @@ -279,7 +279,7 @@
     1.4    | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
     1.5    | add_type_constraint _ = I
     1.6  
     1.7 -fun fix_atp_variable_name f s =
     1.8 +fun repair_atp_variable_name f s =
     1.9    let
    1.10      fun subscript_name s n = s ^ nat_subscript n
    1.11      val s = String.map f s
    1.12 @@ -349,10 +349,10 @@
    1.13                    SOME b => Var ((b, 0), T)
    1.14                  | NONE =>
    1.15                    if is_tptp_variable a then
    1.16 -                    Var ((fix_atp_variable_name Char.toLower a, 0), T)
    1.17 +                    Var ((repair_atp_variable_name Char.toLower a, 0), T)
    1.18                    else
    1.19                      (* Skolem constants? *)
    1.20 -                    Var ((fix_atp_variable_name Char.toUpper a, 0), T)
    1.21 +                    Var ((repair_atp_variable_name Char.toUpper a, 0), T)
    1.22            in list_comb (t, ts) end
    1.23    in aux (SOME HOLogic.boolT) [] end
    1.24  
    1.25 @@ -411,7 +411,8 @@
    1.26          do_formula pos (AQuant (q, xs, phi'))
    1.27          #>> quantify_over_free (case q of
    1.28                                    AForall => @{const_name All}
    1.29 -                                | AExists => @{const_name Ex}) x
    1.30 +                                | AExists => @{const_name Ex})
    1.31 +                               (repair_atp_variable_name Char.toLower x)
    1.32        | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
    1.33        | AConn (c, [phi1, phi2]) =>
    1.34          do_formula (pos |> c = AImplies ? not) phi1
    1.35 @@ -835,6 +836,7 @@
    1.36        second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
    1.37    in proof_top @ proof_bottom end
    1.38  
    1.39 +(* FIXME: Still needed? Probably not. *)
    1.40  val kill_duplicate_assumptions_in_proof =
    1.41    let
    1.42      fun relabel_facts subst =