--- a/src/HOL/Tools/metis_tools.ML Fri May 16 23:25:37 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML Sat May 17 13:54:30 2008 +0200
@@ -270,7 +270,7 @@
fun print_thpair (fth,th) =
(Output.debug (fn () => "=============================================");
Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
- Output.debug (fn () => "Isabelle: " ^ string_of_thm th));
+ Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm th));
fun lookth thpairs (fth : Metis.Thm.thm) =
valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
@@ -309,7 +309,7 @@
in SOME (cterm_of thy v, t) end
handle Option =>
(Output.debug (fn() => "List.find failed for the variable " ^ x ^
- " in " ^ string_of_thm i_th);
+ " in " ^ Display.string_of_thm i_th);
NONE)
fun remove_typeinst (a, t) =
case Recon.strip_prefix ResClause.schematic_var_prefix a of
@@ -317,15 +317,15 @@
| NONE => case Recon.strip_prefix ResClause.tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
- val _ = Output.debug (fn () => " isa th: " ^ string_of_thm i_th)
+ val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm i_th)
val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
val tms = infer_types ctxt rawtms;
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = Output.debug (fn() => "subst_translations:")
- val _ = app (fn (x,y) => Output.debug (fn () => string_of_cterm x ^ " |-> " ^
- string_of_cterm y))
+ val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^
+ Display.string_of_cterm y))
substs'
in cterm_instantiate substs' i_th end;
@@ -347,8 +347,8 @@
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
- val _ = Output.debug (fn () => " isa th1 (pos): " ^ string_of_thm i_th1)
- val _ = Output.debug (fn () => " isa th2 (neg): " ^ string_of_thm i_th2)
+ val _ = Output.debug (fn () => " isa th1 (pos): " ^ Display.string_of_thm i_th1)
+ val _ = Output.debug (fn () => " isa th2 (neg): " ^ Display.string_of_thm i_th2)
in
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
else if is_TrueI i_th2 then i_th1
@@ -425,7 +425,7 @@
val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
- val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst')
+ val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
val eq_terms = map (pairself (cterm_of thy))
(ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
in cterm_instantiate eq_terms subst' end;
@@ -453,7 +453,7 @@
val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf)))
- val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th)
+ val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
val _ = Output.debug (fn () => "=============================================")
val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
in
@@ -572,9 +572,9 @@
val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
else ();
val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
- val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls
val _ = Output.debug (fn () => "THEOREM CLAUSES")
- val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) ths
val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (Output.debug (fn () => "TFREE CLAUSES");
@@ -597,13 +597,13 @@
val result = translate isFO ctxt' axioms proof
and used = List.mapPartial (used_axioms axioms) proof
val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
- val _ = app (fn th => Output.debug (fn () => string_of_thm th)) used
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) used
val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
in
if null unused then ()
else warning ("Unused theorems: " ^ commas (map #1 unused));
case result of
- (_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith)
+ (_,ith)::_ => (Output.debug (fn () => "success: " ^ Display.string_of_thm ith); ith)
| _ => error "METIS: no result"
end
| Metis.Resolution.Satisfiable _ => error "Metis: No first-order proof with the lemmas supplied"
@@ -611,7 +611,7 @@
fun metis_general_tac mode ctxt ths i st0 =
let val _ = Output.debug (fn () =>
- "Metis called with theorems " ^ cat_lines (map string_of_thm ths))
+ "Metis called with theorems " ^ cat_lines (map Display.string_of_thm ths))
in
if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
then error "Proof state contains the empty sort" else ();