1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jan 15 20:51:30 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jan 15 20:51:30 2013 +0100
     1.3 @@ -365,8 +365,11 @@
     1.4     clsarity). *)
     1.5  fun is_only_type_information t = t aconv @{term True}
     1.6  
     1.7 +fun s_maybe_not role = role <> Conjecture ? s_not
     1.8 +
     1.9  fun is_same_inference _ (Definition_Step _) = false
    1.10 -  | is_same_inference t (Inference_Step (_, _, t', _, _)) = t aconv t'
    1.11 +  | is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) =
    1.12 +    s_maybe_not role t aconv s_maybe_not role' t'
    1.13  
    1.14  (* Discard facts; consolidate adjacent lines that prove the same formula, since
    1.15     they differ only in type information.*)
    1.16 @@ -375,18 +378,14 @@
    1.17               lines =
    1.18      (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
    1.19         definitions. *)
    1.20 -    if is_fact fact_names ss then
    1.21 +    if is_conjecture ss then
    1.22 +      Inference_Step (name, role, t, rule, []) :: lines
    1.23 +    else if is_fact fact_names ss then
    1.24        (* Facts are not proof lines. *)
    1.25        if is_only_type_information t then
    1.26          map (replace_dependencies_in_line (name, [])) lines
    1.27 -      (* Is there a repetition? If so, replace later line by earlier one. *)
    1.28 -      else case take_prefix (not o is_same_inference t) lines of
    1.29 -        (_, []) => lines (* no repetition of proof line *)
    1.30 -      | (pre, Inference_Step (name', _, _, _, _) :: post) =>
    1.31 -        pre @ map (replace_dependencies_in_line (name', [name])) post
    1.32 -      | _ => raise Fail "unexpected inference"
    1.33 -    else if is_conjecture ss then
    1.34 -      Inference_Step (name, role, t, rule, []) :: lines
    1.35 +      else
    1.36 +        lines
    1.37      else
    1.38        map (replace_dependencies_in_line (name, [])) lines
    1.39    | add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines =
    1.40 @@ -394,7 +393,7 @@
    1.41      if is_only_type_information t then
    1.42        line :: lines
    1.43      (* Is there a repetition? If so, replace later line by earlier one. *)
    1.44 -    else case take_prefix (not o is_same_inference t) lines of
    1.45 +    else case take_prefix (not o is_same_inference (role, t)) lines of
    1.46        (* FIXME: Doesn't this code risk conflating proofs involving different
    1.47           types? *)
    1.48        (_, []) => line :: lines
    1.49 @@ -406,8 +405,8 @@
    1.50  
    1.51  val repair_waldmeister_endgame =
    1.52    let
    1.53 -    fun do_tail (Inference_Step (name, role, t, rule, deps)) =
    1.54 -        Inference_Step (name, role, s_not t, rule, deps)
    1.55 +    fun do_tail (Inference_Step (name, _, t, rule, deps)) =
    1.56 +        Inference_Step (name, Negated_Conjecture, s_not t, rule, deps)
    1.57        | do_tail line = line
    1.58      fun do_body [] = []
    1.59        | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
    1.60 @@ -652,8 +651,8 @@
    1.61            |> nasty_atp_proof pool
    1.62            |> map_term_names_in_atp_proof repair_name
    1.63            |> decode_lines ctxt sym_tab
    1.64 +          |> repair_waldmeister_endgame
    1.65            |> rpair [] |-> fold_rev (add_line fact_names)
    1.66 -          |> repair_waldmeister_endgame
    1.67            |> rpair [] |-> fold_rev add_nontrivial_line
    1.68            |> rpair (0, [])
    1.69            |-> fold_rev (add_desired_line fact_names frees)
    1.70 @@ -685,7 +684,7 @@
    1.71                      | Inference_Step (name as (s, ss), role, t, rule, _) =>
    1.72                        Symtab.update_new (s, (rule,
    1.73                          t |> (if member (op = o apsnd fst) tainted s then
    1.74 -                                (role <> Conjecture ? s_not)
    1.75 +                                s_maybe_not role
    1.76                                  #> fold exists_of (map Var (Term.add_vars t []))
    1.77                                else
    1.78                                  I))))
    1.79 @@ -726,9 +725,9 @@
    1.80              in
    1.81                if is_clause_skolemize_rule c then
    1.82                  let
    1.83 -                  val xs =
    1.84 -                    Term.add_frees t []
    1.85 -                    |> filter_out (Variable.is_declared ctxt o fst)
    1.86 +                  val is_fixed =
    1.87 +                    Variable.is_declared ctxt orf can Name.dest_skolem
    1.88 +                  val xs = Term.add_frees t [] |> filter_out (is_fixed o fst)
    1.89                  in Obtain ([], xs, l, t, by) end
    1.90                else
    1.91                  Prove (maybe_show outer c [], l, t, by)