1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -18,7 +18,8 @@
     1.4    val verbose : bool Config.T
     1.5    val verbose_warning : Proof.context -> string -> unit
     1.6    val hol_clause_from_metis :
     1.7 -    Proof.context -> int Symtab.table -> Metis_Thm.thm -> term
     1.8 +    Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
     1.9 +    -> term
    1.10    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    1.11    val untyped_aconv : term * term -> bool
    1.12    val replay_one_inference :
    1.13 @@ -74,7 +75,7 @@
    1.14    end;
    1.15  
    1.16  fun infer_types ctxt =
    1.17 -  Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt);
    1.18 +  Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    1.19  
    1.20  (* We use 1 rather than 0 because variable references in clauses may otherwise
    1.21     conflict with variable constraints in the goal...at least, type inference
    1.22 @@ -223,7 +224,8 @@
    1.23    | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
    1.24  
    1.25  fun hol_term_from_metis_MX ctxt sym_tab =
    1.26 -  atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
    1.27 +  atp_term_from_metis
    1.28 +  #> term_from_atp ctxt false sym_tab NONE
    1.29  
    1.30  fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt
    1.31    | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt
    1.32 @@ -236,19 +238,24 @@
    1.33    | atp_clause_from_metis lits =
    1.34      lits |> map atp_literal_from_metis |> mk_aconns AOr
    1.35  
    1.36 -fun hol_clause_from_metis ctxt sym_tab =
    1.37 +fun reveal_old_skolems_and_infer_types ctxt old_skolems =
    1.38 +  map (reveal_old_skolem_terms old_skolems)
    1.39 +  #> infer_types ctxt
    1.40 +
    1.41 +fun hol_clause_from_metis ctxt sym_tab old_skolems =
    1.42    Metis_Thm.clause
    1.43    #> Metis_LiteralSet.toList
    1.44    #> atp_clause_from_metis
    1.45    #> prop_from_atp ctxt false sym_tab
    1.46 +  #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
    1.47  
    1.48  fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
    1.49    let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms
    1.50        val _ = trace_msg ctxt (fn () => "  calling type inference:")
    1.51        val _ = app (fn t => trace_msg ctxt
    1.52                                       (fn () => Syntax.string_of_term ctxt t)) ts
    1.53 -      val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
    1.54 -                   |> infer_types ctxt
    1.55 +      val ts' =
    1.56 +        ts |> reveal_old_skolems_and_infer_types ctxt old_skolems
    1.57        val _ = app (fn t => trace_msg ctxt
    1.58                      (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
    1.59                                " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
    1.60 @@ -308,7 +315,7 @@
    1.61        fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
    1.62        fun subst_translation (x,y) =
    1.63          let val v = find_var x
    1.64 -            (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
    1.65 +            (* We call "reveal_old_skolems_and_infer_types" below. *)
    1.66              val t = hol_term_from_metis ctxt mode sym_tab y
    1.67          in  SOME (cterm_of thy (Var v), t)  end
    1.68          handle Option.Option =>
    1.69 @@ -327,9 +334,9 @@
    1.70                | NONE => SOME (a,t)    (*internal Metis var?*)
    1.71        val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
    1.72        val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
    1.73 -      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
    1.74 -      val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
    1.75 -                       |> infer_types ctxt
    1.76 +      val (vars, tms) =
    1.77 +        ListPair.unzip (map_filter subst_translation substs)
    1.78 +        ||> reveal_old_skolems_and_infer_types ctxt old_skolems
    1.79        val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
    1.80        val substs' = ListPair.zip (vars, map ctm_of tms)
    1.81        val _ = trace_msg ctxt (fn () =>