# HG changeset patch # User wenzelm # Date 1129911278 -7200 # Node ID 8db36a1082132c871d20a93f3826f73fb662e7a7 # Parent c0bc47e944de4d40514226cd979506e73ab58a2c OldGoals; diff -r c0bc47e944de -r 8db36a108213 TFL/post.ML --- 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))); diff -r c0bc47e944de -r 8db36a108213 TFL/rules.ML --- 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; diff -r c0bc47e944de -r 8db36a108213 src/HOL/Import/proof_kernel.ML --- 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. *) diff -r c0bc47e944de -r 8db36a108213 src/HOL/Import/replay.ML --- 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 diff -r c0bc47e944de -r 8db36a108213 src/HOL/Import/shuffler.ML --- 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 diff -r c0bc47e944de -r 8db36a108213 src/HOL/Integ/cooper_proof.ML --- 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; (*-------------------------------------------------------------*) diff -r c0bc47e944de -r 8db36a108213 src/HOL/Modelcheck/mucke_oracle.ML --- 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 ) diff -r c0bc47e944de -r 8db36a108213 src/HOL/Tools/Presburger/cooper_proof.ML --- 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; (*-------------------------------------------------------------*) diff -r c0bc47e944de -r 8db36a108213 src/HOL/Tools/datatype_abs_proofs.ML --- 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, diff -r c0bc47e944de -r 8db36a108213 src/HOL/Tools/datatype_realizer.ML --- 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 => diff -r c0bc47e944de -r 8db36a108213 src/HOL/Tools/datatype_rep_proofs.ML --- 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, diff -r c0bc47e944de -r 8db36a108213 src/HOL/Tools/inductive_package.ML --- 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 diff -r c0bc47e944de -r 8db36a108213 src/HOL/Tools/inductive_realizer.ML --- 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]), diff -r c0bc47e944de -r 8db36a108213 src/HOL/Tools/primrec_package.ML --- 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'' diff -r c0bc47e944de -r 8db36a108213 src/HOL/Tools/res_axioms.ML --- 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; diff -r c0bc47e944de -r 8db36a108213 src/HOL/arith_data.ML --- 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)))); diff -r c0bc47e944de -r 8db36a108213 src/HOL/simpdata.ML --- 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)))))) diff -r c0bc47e944de -r 8db36a108213 src/HOLCF/IOA/Modelcheck/MuIOA.ML --- 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) diff -r c0bc47e944de -r 8db36a108213 src/HOLCF/domain/theorems.ML --- 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); diff -r c0bc47e944de -r 8db36a108213 src/HOLCF/fixrec_package.ML --- 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; diff -r c0bc47e944de -r 8db36a108213 src/Provers/splitter.ML --- 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; diff -r c0bc47e944de -r 8db36a108213 src/Pure/proof_general.ML --- 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; diff -r c0bc47e944de -r 8db36a108213 src/ZF/Tools/datatype_package.ML --- 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]); diff -r c0bc47e944de -r 8db36a108213 src/ZF/Tools/inductive_package.ML --- 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, diff -r c0bc47e944de -r 8db36a108213 src/ZF/Tools/primrec_package.ML --- 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);