Superficial changes
authorpaulson
Mon Apr 07 15:37:04 2008 +0200 (2008-04-07)
changeset 26561394cd765643d
parent 26560 d2fc9a18ee8a
child 26562 9d25ef112cf6
Superficial changes
CVS: ----------------------------------------------------------------------
src/HOL/Tools/metis_tools.ML
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Fri Apr 04 13:40:27 2008 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Mon Apr 07 15:37:04 2008 +0200
     1.3 @@ -295,17 +295,17 @@
     1.4        (ProofContext.theory_of ctxt)
     1.5        (singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm));
     1.6  
     1.7 -  (* INFERENCE RULE: INSTANTIATE. Type instantiations are ignored. Attempting to reconstruct
     1.8 +  (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
     1.9       them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
    1.10       that new TVars are distinct and that types can be inferred from terms.*)
    1.11 -  fun inst_inf ctxt thpairs fsubst th =
    1.12 +  fun inst_inf ctxt thpairs fsubst th =    
    1.13      let val thy = ProofContext.theory_of ctxt
    1.14          val i_th   = lookth thpairs th
    1.15          val i_th_vars = term_vars (prop_of i_th)
    1.16          fun find_var x = valOf (List.find (fn Term.Var((a,_),_) => a=x) i_th_vars)
    1.17          fun subst_translation (x,y) =
    1.18                let val v = find_var x
    1.19 -                  val t = fol_term_to_hol_RAW ctxt y
    1.20 +                  val t = fol_term_to_hol_RAW ctxt y (*we call infer_types below*)
    1.21                in  SOME (cterm_of thy v, t)  end
    1.22                handle Option =>
    1.23                    (Output.debug (fn() => "List.find failed for the variable " ^ x ^
    1.24 @@ -606,7 +606,7 @@
    1.25                        (_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith)
    1.26                      | _ => error "METIS: no result"
    1.27                end
    1.28 -          | Metis.Resolution.Satisfiable _ => error "Metis finds the theorem to be invalid"
    1.29 +          | Metis.Resolution.Satisfiable _ => error "Metis: No first-order proof with the lemmas supplied"
    1.30      end;
    1.31  
    1.32    fun metis_general_tac mode ctxt ths i st0 =