diff -r 8684b5240f11 -r ca87aff1ad2d src/HOL/Tools/metis_tools.ML --- 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 ();