--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 16:50:14 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 16:50:14 2013 +0100
@@ -72,7 +72,7 @@
(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
type information. *)
-fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines =
+fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
definitions. *)
if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
@@ -94,7 +94,7 @@
fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) []
fun add_lines_pass3 res [] = rev res
- | add_lines_pass3 res ((name as (_, ss), role, t, rule, deps) :: lines) =
+ | add_lines_pass3 res ((name, role, t, rule, deps) :: lines) =
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
(* the last line must be kept *)
null lines orelse
@@ -208,7 +208,7 @@
atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
- val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
+ val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
val (_, ctxt) =
params
|> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))