src/HOL/Tools/Metis/metis_tactics.ML
changeset 42341 5a00af7f4978
parent 42336 d63d43e85879
child 42361 23f352990944
     1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Apr 14 11:24:04 2011 +0200
     1.3 @@ -92,11 +92,9 @@
     1.4                            Metis_Thm.toString mth)
     1.5                  val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
     1.6                               (*add constraints arising from converting goal to clause form*)
     1.7 -                val new_skolem_var_count = Unsynchronized.ref 1
     1.8                  val proof = Metis_Proof.proof mth
     1.9 -                val result =
    1.10 -                  fold (replay_one_inference ctxt' mode
    1.11 -                              (old_skolems, new_skolem_var_count)) proof axioms
    1.12 +                val result = fold (replay_one_inference ctxt' mode old_skolems)
    1.13 +                                  proof axioms
    1.14                  and used = map_filter (used_axioms axioms) proof
    1.15                  val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    1.16                  val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used