--- a/TFL/post.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/TFL/post.ML Fri Oct 21 18:14:38 2005 +0200
@@ -52,7 +52,7 @@
fun tgoalw thy defs rules =
case termination_goals rules of
[] => error "tgoalw: no termination conditions to prove"
- | L => goalw_cterm defs
+ | L => OldGoals.goalw_cterm defs
(Thm.cterm_of (Theory.sign_of thy)
(HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
--- a/TFL/rules.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/TFL/rules.ML Fri Oct 21 18:14:38 2005 +0200
@@ -815,10 +815,10 @@
fun prove strict (ptm, tac) =
let val result =
- if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac])
+ if strict then OldGoals.prove_goalw_cterm [] ptm (fn _ => [tac])
else
transform_error (fn () =>
- Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
+ OldGoals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
in #1 (freeze_thaw result) end;
--- a/src/HOL/Import/proof_kernel.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Oct 21 18:14:38 2005 +0200
@@ -172,7 +172,7 @@
fun print_exn e =
case e of
PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
- | _ => Goals.print_exn e
+ | _ => OldGoals.print_exn e
(* Compatibility. *)
--- a/src/HOL/Import/replay.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Import/replay.ML Fri Oct 21 18:14:38 2005 +0200
@@ -270,7 +270,7 @@
| _ => rp pc thy
end
in
- rp' prf thy handle e => (writeln "Exception in replay_proof"; print_exn e)
+ rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
end
fun setup_int_thms thyname thy =
@@ -344,4 +344,4 @@
replay_fact (thmname,thy)
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Import/shuffler.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Import/shuffler.ML Fri Oct 21 18:14:38 2005 +0200
@@ -223,7 +223,7 @@
val rew = Logic.mk_equals (lhs,rhs)
val init = trivial (cterm_of sg rew)
in
- (all_comm RS init handle e => (message "rew_th"; print_exn e))
+ (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
end
fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
@@ -343,7 +343,7 @@
SOME res
end
else NONE)
- handle e => print_exn e)
+ handle e => OldGoals.print_exn e)
| _ => NONE
end
@@ -411,7 +411,7 @@
else NONE
| _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
end
- handle e => (writeln "eta_expand internal error";print_exn e)
+ handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
fun mk_tfree s = TFree("'"^s,[])
val xT = mk_tfree "a"
@@ -524,7 +524,7 @@
in
Drule.forall_intr_list (map (cterm_of sg) vars) th
end
- handle e => (writeln "close_thm internal error"; print_exn e)
+ handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
(* Normalizes a theorem's conclusion using norm_term. *)
@@ -622,7 +622,7 @@
else error "Internal error in set_prop"
| NONE => NONE
end
- handle e => (writeln "set_prop internal error"; print_exn e)
+ handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
fun find_potential thy t =
let
--- a/src/HOL/Integ/cooper_proof.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Integ/cooper_proof.ML Fri Oct 21 18:14:38 2005 +0200
@@ -197,7 +197,7 @@
fun check NONE = error "prove_goal: tactic failed"
| check (SOME (thm, _)) = (case nprems_of thm of
0 => thm
- | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
+ | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!"))
in check (Seq.pull (EVERY tacs (trivial G))) end;
(*-------------------------------------------------------------*)
--- a/src/HOL/Modelcheck/mucke_oracle.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Fri Oct 21 18:14:38 2005 +0200
@@ -109,14 +109,14 @@
val trm = hd(itrm)
in
(
-push_proof();
-goalw_cterm [] (cterm_of sign trm);
+OldGoals.push_proof();
+OldGoals.goalw_cterm [] (cterm_of sign trm);
by (simp_tac (simpset()) 1);
let
val if_tmp_result = result()
in
(
- pop_proof();
+ OldGoals.pop_proof();
CHANGED(full_simp_tac (sset addsimps [if_tmp_result]) i) state)
end
)
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Fri Oct 21 18:14:38 2005 +0200
@@ -197,7 +197,7 @@
fun check NONE = error "prove_goal: tactic failed"
| check (SOME (thm, _)) = (case nprems_of thm of
0 => thm
- | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
+ | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!"))
in check (Seq.pull (EVERY tacs (trivial G))) end;
(*-------------------------------------------------------------*)
--- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 21 18:14:38 2005 +0200
@@ -73,7 +73,7 @@
val induct' = refl RS ((List.nth
(split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
- in prove_goalw_cterm [] (cert t) (fn prems =>
+ in OldGoals.prove_goalw_cterm [] (cert t) (fn prems =>
[rtac induct' 1,
REPEAT (rtac TrueI 1),
REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
@@ -211,7 +211,7 @@
THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
- in split_conj_thm (prove_goalw_cterm []
+ in split_conj_thm (OldGoals.prove_goalw_cterm []
(cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
end;
@@ -244,7 +244,7 @@
val _ = message "Proving characteristic theorems for primrec combinators ..."
- val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
+ val rec_thms = map (fn t => OldGoals.prove_goalw_cterm reccomb_defs
(cterm_of (Theory.sign_of thy2) t) (fn _ =>
[rtac the1_equality 1,
resolve_tac rec_unique_thms 1,
@@ -318,7 +318,7 @@
end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
(Library.take (length newTs, reccomb_names)));
- val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
+ val case_thms = map (map (fn t => OldGoals.prove_goalw_cterm (case_defs @
(map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t)
(fn _ => [rtac refl 1])))
(DatatypeProp.make_cases new_type_names descr sorts thy2)
@@ -352,8 +352,8 @@
val tacsf = K [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
(HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))]
in
- (prove_goalw_cterm [] (cert t1) tacsf,
- prove_goalw_cterm [] (cert t2) tacsf)
+ (OldGoals.prove_goalw_cterm [] (cert t1) tacsf,
+ OldGoals.prove_goalw_cterm [] (cert t2) tacsf)
end;
val split_thm_pairs = map prove_split_thms
@@ -419,7 +419,7 @@
val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
- val size_thms = map (fn t => prove_goalw_cterm rewrites
+ val size_thms = map (fn t => OldGoals.prove_goalw_cterm rewrites
(cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1]))
(DatatypeProp.make_size descr sorts thy')
@@ -432,7 +432,7 @@
fun prove_weak_case_congs new_type_names descr sorts thy =
let
fun prove_weak_case_cong t =
- prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t)
+ OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t)
(fn prems => [rtac ((hd prems) RS arg_cong) 1])
val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
@@ -453,7 +453,7 @@
hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
| tac i n = rtac disjI2 i THEN tac i (n - 1)
in
- prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ =>
+ OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ =>
[rtac allI 1,
exh_tac (K exhaustion) 1,
ALLGOALS (fn i => tac i (i-1))])
@@ -475,7 +475,7 @@
val nchotomy'' = cterm_instantiate
[(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
in
- prove_goalw_cterm [] (cert t) (fn prems =>
+ OldGoals.prove_goalw_cterm [] (cert t) (fn prems =>
let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
in [simp_tac (HOL_ss addsimps [hd prems]) 1,
cut_facts_tac [nchotomy''] 1,
--- a/src/HOL/Tools/datatype_realizer.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Oct 21 18:14:38 2005 +0200
@@ -119,7 +119,7 @@
val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
- val thm = simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
+ val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
(fn prems =>
[rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
rtac (cterm_instantiate inst induction) 1,
@@ -190,7 +190,7 @@
val y = Var (("y", 0), Type.varifyT T);
val y' = Free ("y", T);
- val thm = prove_goalw_cterm [] (cert (Logic.list_implies (prems,
+ val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
list_comb (r, rs @ [y'])))))
(fn prems =>
--- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Oct 21 18:14:38 2005 +0200
@@ -279,7 +279,7 @@
val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
val inj_Abs_thm =
- prove_goalw_cterm []
+ OldGoals.prove_goalw_cterm []
(cterm_of sg
(HOLogic.mk_Trueprop
(Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
@@ -289,7 +289,7 @@
val setT = HOLogic.mk_setT T
val inj_Rep_thm =
- prove_goalw_cterm []
+ OldGoals.prove_goalw_cterm []
(cterm_of sg
(HOLogic.mk_Trueprop
(Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
@@ -375,7 +375,7 @@
(* prove characteristic equations *)
val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
- val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
+ val char_thms' = map (fn eqn => OldGoals.prove_goalw_cterm rewrites
(cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
in (thy', char_thms' @ char_thms) end;
@@ -397,7 +397,7 @@
val Ts = map (TFree o rpair HOLogic.typeS)
(variantlist (replicate i "'t", used));
val f = Free ("f", Ts ---> U)
- in prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
+ in OldGoals.prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.list_all
(map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
@@ -431,7 +431,7 @@
val inj_thms' = map (fn r => r RS injD)
(map snd newT_iso_inj_thms @ inj_thms);
- val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
+ val inj_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
(HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
[(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
REPEAT (EVERY
@@ -457,7 +457,7 @@
(split_conj_thm inj_thm);
val elem_thm =
- prove_goalw_cterm []
+ OldGoals.prove_goalw_cterm []
(cterm_of (Theory.sign_of thy5)
(HOLogic.mk_Trueprop (mk_conj ind_concl2)))
(fn _ =>
@@ -495,7 +495,7 @@
val iso_thms = if length descr = 1 then [] else
Library.drop (length newTs, split_conj_thm
- (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
+ (OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
[(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq choice_eq ::
@@ -525,7 +525,7 @@
let
val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
- in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
+ in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
rtac refl 1,
@@ -547,7 +547,7 @@
fun prove_distinct_thms (_, []) = []
| prove_distinct_thms (dist_rewrites', t::_::ts) =
let
- val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
+ val dist_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
[simp_tac (HOL_ss addsimps dist_rewrites') 1])
in dist_thm::(standard (dist_thm RS not_sym))::
(prove_distinct_thms (dist_rewrites', ts))
@@ -568,7 +568,7 @@
((map (fn r => r RS injD) iso_inj_thms) @
[In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
Lim_inject, Suml_inject, Sumr_inject]))
- in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
+ in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
[rtac iffI 1,
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
dresolve_tac rep_congs 1, dtac box_equals 1,
@@ -616,7 +616,7 @@
val cert = cterm_of (Theory.sign_of thy6);
- val indrule_lemma = prove_goalw_cterm [] (cert
+ val indrule_lemma = OldGoals.prove_goalw_cterm [] (cert
(Logic.mk_implies
(HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls)))) (fn prems =>
@@ -630,7 +630,7 @@
map (Free o apfst fst o dest_Var) Ps;
val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
- val dt_induct = prove_goalw_cterm [] (cert
+ val dt_induct = OldGoals.prove_goalw_cterm [] (cert
(DatatypeProp.make_ind descr sorts)) (fn prems =>
[rtac indrule_lemma' 1,
(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
--- a/src/HOL/Tools/inductive_package.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Fri Oct 21 18:14:38 2005 +0200
@@ -472,7 +472,7 @@
fun prove_mono setT fp_fun monos thy =
(message " Proving monotonicity ...";
- Goals.prove_goalw_cterm [] (*NO quick_and_dirty_prove_goalw_cterm here!*)
+ OldGoals.prove_goalw_cterm [] (*NO quick_and_dirty_prove_goalw_cterm here!*)
(Thm.cterm_of thy (HOLogic.mk_Trueprop
(Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
(fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
@@ -491,7 +491,7 @@
| select_disj _ 1 = [rtac disjI1]
| select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
- val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
+ val intrs = map (fn (i, intr) => OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
(Thm.cterm_of thy intr) (fn prems =>
[(*insert prems and underlying sets*)
cut_facts_tac prems 1,
@@ -519,7 +519,7 @@
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
in
mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
- quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
+ OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
(Thm.cterm_of thy t) (fn prems =>
[cut_facts_tac [hd prems] 1,
dtac (unfold RS subst) 1,
@@ -648,7 +648,7 @@
(* simplification rules for vimage and Collect *)
val vimage_simps = if length cs < 2 then [] else
- map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
+ map (fn c => OldGoals.quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
@@ -661,7 +661,7 @@
(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
else ();
- val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
+ val induct = OldGoals.quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
(Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
[rtac (impI RS allI) 1,
DETERM (etac raw_fp_induct 1),
@@ -676,7 +676,7 @@
EVERY (map (fn prem =>
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
- val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
+ val lemma = OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
[cut_facts_tac prems 1,
REPEAT (EVERY
--- a/src/HOL/Tools/inductive_realizer.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Oct 21 18:14:38 2005 +0200
@@ -360,7 +360,7 @@
(Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
val rews = map mk_meta_eq
(fst_conv :: snd_conv :: get #rec_thms dt_info);
- val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
+ val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
[if length rss = 1 then
cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
else EVERY [rewrite_goals_tac (rews @ all_simps),
@@ -410,7 +410,7 @@
val rlz = strip_all (Logic.unvarify
(Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
val rews = map mk_meta_eq case_thms;
- val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
+ val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
[cut_facts_tac [hd prems] 1,
etac elimR 1,
ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
--- a/src/HOL/Tools/primrec_package.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML Fri Oct 21 18:14:38 2005 +0200
@@ -254,7 +254,7 @@
val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
val _ = message ("Proving equations for primrec function(s) " ^
commas_quote (map fst nameTs1) ^ " ...");
- val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
+ val simps = map (fn (_, t) => OldGoals.prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
(fn _ => [rtac refl 1])) eqns;
val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
val thy''' = thy''
--- a/src/HOL/Tools/res_axioms.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Oct 21 18:14:38 2005 +0200
@@ -130,7 +130,7 @@
let val tm = elimR2Fol th
val ctm = cterm_of (sign_of_thm th) tm
in
- prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
+ OldGoals.prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
end
else th;
@@ -240,7 +240,7 @@
val cex = Thm.cterm_of sign (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
- in prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc))
+ in OldGoals.prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc))
(fn [prem] => [ rtac (prem RS someI_ex) 1 ])
end;
--- a/src/HOL/arith_data.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/arith_data.ML Fri Oct 21 18:14:38 2005 +0200
@@ -52,7 +52,7 @@
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
fun prove_conv expand_tac norm_tac sg ss tu =
- mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
+ mk_meta_eq (OldGoals.prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
(K [expand_tac, norm_tac ss]))
handle ERROR => error ("The error(s) above occurred while trying to prove " ^
(string_of_cterm (cterm_of sg (mk_eqv tu))));
--- a/src/HOL/simpdata.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/simpdata.ML Fri Oct 21 18:14:38 2005 +0200
@@ -253,7 +253,7 @@
val aT = TFree ("'a", HOLogic.typeS);
val x = Free ("x", aT);
val y = Free ("y", aT)
- in prove_goalw_cterm [simp_implies_def]
+ in OldGoals.prove_goalw_cterm [simp_implies_def]
(cterm_of sign (Logic.mk_implies
(mk_simp_implies (Logic.mk_equals (x, y)),
mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))))
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML Fri Oct 21 18:14:38 2005 +0200
@@ -226,7 +226,7 @@
structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
in
(
-push_proof();
+OldGoals.push_proof();
Goal
( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
"))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^
@@ -271,7 +271,7 @@
(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
by (atac 1);
result();
-pop_proof();
+OldGoals.pop_proof();
Logic.strip_imp_concl subgoal
)
end)
--- a/src/HOLCF/domain/theorems.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML Fri Oct 21 18:14:38 2005 +0200
@@ -24,7 +24,7 @@
fun pg'' thy defs t = let val sg = sign_of thy;
val ct = Thm.cterm_of sg (inferT sg t);
- in prove_goalw_cterm defs ct end;
+ in OldGoals.prove_goalw_cterm defs ct end;
fun pg' thy defs t tacsf=pg'' thy defs t (fn [] => tacsf
| prems=> (cut_facts_tac prems 1)::tacsf);
--- a/src/HOLCF/fixrec_package.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOLCF/fixrec_package.ML Fri Oct 21 18:14:38 2005 +0200
@@ -107,7 +107,7 @@
fun mk_cterm t = cterm_of thy' (infer thy' t);
val ctuple_unfold_ct = mk_cterm (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
- val ctuple_unfold_thm = prove_goalw_cterm [] ctuple_unfold_ct
+ val ctuple_unfold_thm = OldGoals.prove_goalw_cterm [] ctuple_unfold_ct
(fn _ => [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
simp_tac (simpset_of thy') 1]);
val ctuple_induct_thm =
@@ -218,7 +218,7 @@
let
fun tacsf prems =
[rtac (unfold_thm RS ssubst_lhs) 1, simp_tac (simpset_of thy addsimps prems) 1];
- fun prove_term t = prove_goalw_cterm [] (cterm_of thy t) tacsf;
+ fun prove_term t = OldGoals.prove_goalw_cterm [] (cterm_of thy t) tacsf;
fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
in
map prove_eqn eqns
@@ -275,7 +275,7 @@
val cname = case chead_of t of Const(c,_) => c | _ =>
fixrec_err "function is not declared as constant in theory";
val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
- val simp = prove_goalw_cterm [] (cterm_of thy eq)
+ val simp = OldGoals.prove_goalw_cterm [] (cterm_of thy eq)
(fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
in simp end;
--- a/src/Provers/splitter.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/Provers/splitter.ML Fri Oct 21 18:14:38 2005 +0200
@@ -73,7 +73,7 @@
let val ct = read_cterm (#sign(rep_thm Data.iffD))
("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \
\P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
- in prove_goalw_cterm [] ct
+ in OldGoals.prove_goalw_cterm [] ct
(fn [prem] => [rewtac prem, rtac reflexive_thm 1])
end;
--- a/src/Pure/proof_general.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/Pure/proof_general.ML Fri Oct 21 18:14:38 2005 +0200
@@ -370,7 +370,7 @@
val help = welcome;
val show_context = Context.the_context;
-fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
+fun kill_goal () = (OldGoals.reset_goals (); tell_clear_goals ());
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
--- a/src/ZF/Tools/datatype_package.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/ZF/Tools/datatype_package.ML Fri Oct 21 18:14:38 2005 +0200
@@ -279,7 +279,7 @@
Su.case_inr RS trans] 1)];
fun prove_case_eqn (arg,con_def) =
- prove_goalw_cterm []
+ OldGoals.prove_goalw_cterm []
(Ind_Syntax.traceIt "next case equation = "
(cterm_of (sign_of thy1) (mk_case_eqn arg)))
(case_tacsf con_def);
@@ -324,7 +324,7 @@
IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];
fun prove_recursor_eqn arg =
- prove_goalw_cterm []
+ OldGoals.prove_goalw_cterm []
(Ind_Syntax.traceIt "next recursor equation = "
(cterm_of (sign_of thy1) (mk_recursor_eqn arg)))
recursor_tacsf
@@ -342,7 +342,7 @@
(*Typical theorems have the form ~con1=con2, con1=con2==>False,
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *)
fun mk_free s =
- prove_goalw (theory_of_thm elim) (*Don't use thy1: it will be stale*)
+ OldGoals.prove_goalw (theory_of_thm elim) (*Don't use thy1: it will be stale*)
con_defs s
(fn prems => [cut_facts_tac prems 1,
fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]);
--- a/src/ZF/Tools/inductive_package.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Oct 21 18:14:38 2005 +0200
@@ -192,7 +192,7 @@
val dummy = writeln " Proving monotonicity...";
val bnd_mono =
- prove_goalw_cterm []
+ OldGoals.prove_goalw_cterm []
(cterm_of sign1
(FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
(fn _ =>
@@ -251,7 +251,7 @@
and g rl = rl RS disjI2
in accesses_bal(f, g, asm_rl) end;
- fun prove_intr (ct, tacsf) = prove_goalw_cterm part_rec_defs ct tacsf;
+ fun prove_intr (ct, tacsf) = OldGoals.prove_goalw_cterm part_rec_defs ct tacsf;
val intrs = ListPair.map prove_intr
(map (cterm_of sign1) intr_tms,
@@ -345,7 +345,7 @@
ORELSE' etac FalseE));
val quant_induct =
- prove_goalw_cterm part_rec_defs
+ OldGoals.prove_goalw_cterm part_rec_defs
(cterm_of sign1
(Logic.list_implies
(ind_prems,
@@ -431,7 +431,7 @@
val lemma = (*makes the link between the two induction rules*)
if need_mutual then
(writeln " Proving the mutual induction rule...";
- prove_goalw_cterm part_rec_defs
+ OldGoals.prove_goalw_cterm part_rec_defs
(cterm_of sign1 (Logic.mk_implies (induct_concl,
mutual_induct_concl)))
(fn prems =>
@@ -493,7 +493,7 @@
val mutual_induct_fsplit =
if need_mutual then
- prove_goalw_cterm []
+ OldGoals.prove_goalw_cterm []
(cterm_of sign1
(Logic.list_implies
(map (induct_prem (rec_tms~~preds)) intr_tms,
--- a/src/ZF/Tools/primrec_package.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/ZF/Tools/primrec_package.ML Fri Oct 21 18:14:38 2005 +0200
@@ -182,7 +182,7 @@
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
val eqn_thms =
(message ("Proving equations for primrec function " ^ fname);
- map (fn t => prove_goalw_cterm rewrites
+ map (fn t => OldGoals.prove_goalw_cterm rewrites
(Ind_Syntax.traceIt "next primrec equation = " (cterm_of (sign_of thy1) t))
(fn _ => [rtac refl 1])) eqn_terms);