src/HOL/Tools/Metis/metis_tactics.ML
changeset 40259 c0e34371c2e2
parent 40157 a2f01956220e
child 40262 8403085384eb
     1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Fri Oct 29 12:49:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Fri Oct 29 12:49:05 2010 +0200
     1.3 @@ -91,9 +91,11 @@
     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 old_skolems) proof axioms
    1.11 +                  fold (replay_one_inference ctxt' mode
    1.12 +                              (old_skolems, new_skolem_var_count)) proof axioms
    1.13                  and used = map_filter (used_axioms axioms) proof
    1.14                  val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    1.15                  val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
    1.16 @@ -155,7 +157,7 @@
    1.17        (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
    1.18      else
    1.19        Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
    1.20 -                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
    1.21 +                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt [] (cls @ ths)) 1)
    1.22                    ctxt i st0
    1.23    end
    1.24