1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
     1.5    val untyped_aconv : term -> term -> bool
     1.6    val replay_one_inference :
     1.7 -    Proof.context -> mode -> (string * term) list * int Unsynchronized.ref
     1.8 +    Proof.context -> mode -> (string * term) list
     1.9      -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    1.10      -> (Metis_Thm.thm * thm) list
    1.11    val discharge_skolem_premises :
    1.12 @@ -95,7 +95,7 @@
    1.13          | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
    1.14  
    1.15  (*Maps metis terms to isabelle terms*)
    1.16 -fun hol_term_from_metis_PT ctxt new_skolem_var_count fol_tm =
    1.17 +fun hol_term_from_metis_PT ctxt fol_tm =
    1.18    let val thy = ProofContext.theory_of ctxt
    1.19        val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
    1.20                                         Metis_Term.toString fol_tm)
    1.21 @@ -128,11 +128,9 @@
    1.22                      val nterms = length ts - ntypes
    1.23                      val tts = map tm_to_tt ts
    1.24                      val tys = types_of (List.take(tts,ntypes))
    1.25 -                    val j = !new_skolem_var_count + 0 (* FIXME ### *)
    1.26 -                    val _ = new_skolem_var_count := j
    1.27                      val t =
    1.28                        if String.isPrefix new_skolem_const_prefix c then
    1.29 -                        Var ((new_skolem_var_name_from_const c, j),
    1.30 +                        Var ((new_skolem_var_name_from_const c, 1),
    1.31                               Type_Infer.paramify_vars (tl tys ---> hd tys))
    1.32                        else
    1.33                          Const (c, dummyT)
    1.34 @@ -166,7 +164,7 @@
    1.35    end
    1.36  
    1.37  (*Maps fully-typed metis terms to isabelle terms*)
    1.38 -fun hol_term_from_metis_FT ctxt new_skolem_var_count fol_tm =
    1.39 +fun hol_term_from_metis_FT ctxt fol_tm =
    1.40    let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
    1.41                                         Metis_Term.toString fol_tm)
    1.42        fun do_const c =
    1.43 @@ -204,17 +202,17 @@
    1.44                  SOME v => Free (v, dummyT)
    1.45                | NONE => (trace_msg ctxt (fn () =>
    1.46                                        "hol_term_from_metis_FT bad const: " ^ x);
    1.47 -                         hol_term_from_metis_PT ctxt new_skolem_var_count t))
    1.48 +                         hol_term_from_metis_PT ctxt t))
    1.49          | cvt t = (trace_msg ctxt (fn () =>
    1.50                     "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
    1.51 -                   hol_term_from_metis_PT ctxt new_skolem_var_count t)
    1.52 +                   hol_term_from_metis_PT ctxt t)
    1.53    in fol_tm |> cvt end
    1.54  
    1.55  fun hol_term_from_metis FT = hol_term_from_metis_FT
    1.56    | hol_term_from_metis _ = hol_term_from_metis_PT
    1.57  
    1.58 -fun hol_terms_from_metis ctxt mode (old_skolems, new_skolem_var_count) fol_tms =
    1.59 -  let val ts = map (hol_term_from_metis mode ctxt new_skolem_var_count) fol_tms
    1.60 +fun hol_terms_from_metis ctxt mode old_skolems fol_tms =
    1.61 +  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
    1.62        val _ = trace_msg ctxt (fn () => "  calling type inference:")
    1.63        val _ = app (fn t => trace_msg ctxt
    1.64                                       (fn () => Syntax.string_of_term ctxt t)) ts
    1.65 @@ -271,7 +269,7 @@
    1.66     sorts. Instead we try to arrange that new TVars are distinct and that types
    1.67     can be inferred from terms. *)
    1.68  
    1.69 -fun inst_inf ctxt mode (old_skolems, new_skolem_var_count) thpairs fsubst th =
    1.70 +fun inst_inf ctxt mode old_skolems thpairs fsubst th =
    1.71    let val thy = ProofContext.theory_of ctxt
    1.72        val i_th = lookth thpairs th
    1.73        val i_th_vars = Term.add_vars (prop_of i_th) []
    1.74 @@ -279,7 +277,7 @@
    1.75        fun subst_translation (x,y) =
    1.76          let val v = find_var x
    1.77              (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
    1.78 -            val t = hol_term_from_metis mode ctxt new_skolem_var_count y
    1.79 +            val t = hol_term_from_metis mode ctxt y
    1.80          in  SOME (cterm_of thy (Var v), t)  end
    1.81          handle Option.Option =>
    1.82                 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^

     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Apr 14 11:24:04 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Apr 14 11:24:04 2011 +0200
     2.3 @@ -92,11 +92,9 @@
     2.4                            Metis_Thm.toString mth)
     2.5                  val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
     2.6                               (*add constraints arising from converting goal to clause form*)
     2.7 -                val new_skolem_var_count = Unsynchronized.ref 1
     2.8                  val proof = Metis_Proof.proof mth
     2.9 -                val result =
    2.10 -                  fold (replay_one_inference ctxt' mode
    2.11 -                              (old_skolems, new_skolem_var_count)) proof axioms
    2.12 +                val result = fold (replay_one_inference ctxt' mode old_skolems)
    2.13 +                                  proof axioms
    2.14                  and used = map_filter (used_axioms axioms) proof
    2.15                  val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    2.16                  val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used