OldGoals;
authorwenzelm
Fri Oct 21 18:14:38 2005 +0200 (2005-10-21 ago)
changeset 179598db36a108213
parent 17958 c0bc47e944de
child 17960 5662fa033a92
OldGoals;
TFL/post.ML
TFL/rules.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Import/shuffler.ML
src/HOL/Integ/cooper_proof.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Tools/Presburger/cooper_proof.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/res_axioms.ML
src/HOL/arith_data.ML
src/HOL/simpdata.ML
src/HOLCF/IOA/Modelcheck/MuIOA.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/fixrec_package.ML
src/Provers/splitter.ML
src/Pure/proof_general.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/TFL/post.ML	Fri Oct 21 18:14:37 2005 +0200
     1.2 +++ b/TFL/post.ML	Fri Oct 21 18:14:38 2005 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  fun tgoalw thy defs rules =
     1.5    case termination_goals rules of
     1.6        [] => error "tgoalw: no termination conditions to prove"
     1.7 -    | L  => goalw_cterm defs
     1.8 +    | L  => OldGoals.goalw_cterm defs
     1.9                (Thm.cterm_of (Theory.sign_of thy)
    1.10                          (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
    1.11  
     2.1 --- a/TFL/rules.ML	Fri Oct 21 18:14:37 2005 +0200
     2.2 +++ b/TFL/rules.ML	Fri Oct 21 18:14:38 2005 +0200
     2.3 @@ -815,10 +815,10 @@
     2.4  
     2.5  fun prove strict (ptm, tac) =
     2.6    let val result =
     2.7 -    if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac])
     2.8 +    if strict then OldGoals.prove_goalw_cterm [] ptm (fn _ => [tac])
     2.9      else
    2.10        transform_error (fn () =>
    2.11 -        Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
    2.12 +        OldGoals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
    2.13        handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
    2.14    in #1 (freeze_thaw result) end;
    2.15  
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Oct 21 18:14:37 2005 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Oct 21 18:14:38 2005 +0200
     3.3 @@ -172,7 +172,7 @@
     3.4  fun print_exn e = 
     3.5      case e of
     3.6  	PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
     3.7 -      | _ => Goals.print_exn e
     3.8 +      | _ => OldGoals.print_exn e
     3.9  
    3.10  (* Compatibility. *)
    3.11  
     4.1 --- a/src/HOL/Import/replay.ML	Fri Oct 21 18:14:37 2005 +0200
     4.2 +++ b/src/HOL/Import/replay.ML	Fri Oct 21 18:14:38 2005 +0200
     4.3 @@ -270,7 +270,7 @@
     4.4  		  | _ => rp pc thy
     4.5  	    end
     4.6      in
     4.7 -	rp' prf thy handle e => (writeln "Exception in replay_proof"; print_exn e)
     4.8 +	rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
     4.9      end
    4.10  
    4.11  fun setup_int_thms thyname thy =
    4.12 @@ -344,4 +344,4 @@
    4.13  	replay_fact (thmname,thy)
    4.14      end
    4.15  
    4.16 -end
    4.17 \ No newline at end of file
    4.18 +end
     5.1 --- a/src/HOL/Import/shuffler.ML	Fri Oct 21 18:14:37 2005 +0200
     5.2 +++ b/src/HOL/Import/shuffler.ML	Fri Oct 21 18:14:38 2005 +0200
     5.3 @@ -223,7 +223,7 @@
     5.4  	val rew = Logic.mk_equals (lhs,rhs)
     5.5  	val init = trivial (cterm_of sg rew)
     5.6      in
     5.7 -	(all_comm RS init handle e => (message "rew_th"; print_exn e))
     5.8 +	(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
     5.9      end
    5.10  
    5.11  fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
    5.12 @@ -343,7 +343,7 @@
    5.13  		       SOME res
    5.14  		  end
    5.15  	      else NONE)
    5.16 -	     handle e => print_exn e)
    5.17 +	     handle e => OldGoals.print_exn e)
    5.18  	  | _ => NONE
    5.19         end
    5.20  
    5.21 @@ -411,7 +411,7 @@
    5.22  	    else NONE
    5.23  	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
    5.24      end
    5.25 -    handle e => (writeln "eta_expand internal error";print_exn e)
    5.26 +    handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
    5.27  
    5.28  fun mk_tfree s = TFree("'"^s,[])
    5.29  val xT = mk_tfree "a"
    5.30 @@ -524,7 +524,7 @@
    5.31      in
    5.32  	Drule.forall_intr_list (map (cterm_of sg) vars) th
    5.33      end
    5.34 -    handle e => (writeln "close_thm internal error"; print_exn e)
    5.35 +    handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
    5.36  
    5.37  (* Normalizes a theorem's conclusion using norm_term. *)
    5.38  
    5.39 @@ -622,7 +622,7 @@
    5.40  					else error "Internal error in set_prop"
    5.41  	     | NONE => NONE
    5.42      end
    5.43 -    handle e => (writeln "set_prop internal error"; print_exn e)
    5.44 +    handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
    5.45  
    5.46  fun find_potential thy t =
    5.47      let
     6.1 --- a/src/HOL/Integ/cooper_proof.ML	Fri Oct 21 18:14:37 2005 +0200
     6.2 +++ b/src/HOL/Integ/cooper_proof.ML	Fri Oct 21 18:14:38 2005 +0200
     6.3 @@ -197,7 +197,7 @@
     6.4      fun check NONE = error "prove_goal: tactic failed"
     6.5        | check (SOME (thm, _)) = (case nprems_of thm of
     6.6              0 => thm
     6.7 -          | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
     6.8 +          | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!"))
     6.9    in check (Seq.pull (EVERY tacs (trivial G))) end;
    6.10  
    6.11  (*-------------------------------------------------------------*)
     7.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Fri Oct 21 18:14:37 2005 +0200
     7.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Fri Oct 21 18:14:38 2005 +0200
     7.3 @@ -109,14 +109,14 @@
     7.4  val trm = hd(itrm)
     7.5  in
     7.6  (
     7.7 -push_proof();
     7.8 -goalw_cterm [] (cterm_of sign trm);
     7.9 +OldGoals.push_proof();
    7.10 +OldGoals.goalw_cterm [] (cterm_of sign trm);
    7.11  by (simp_tac (simpset()) 1);
    7.12          let
    7.13          val if_tmp_result = result()
    7.14          in
    7.15          (
    7.16 -        pop_proof();
    7.17 +        OldGoals.pop_proof();
    7.18          CHANGED(full_simp_tac (sset addsimps [if_tmp_result]) i) state)
    7.19          end
    7.20  )
     8.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Fri Oct 21 18:14:37 2005 +0200
     8.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Fri Oct 21 18:14:38 2005 +0200
     8.3 @@ -197,7 +197,7 @@
     8.4      fun check NONE = error "prove_goal: tactic failed"
     8.5        | check (SOME (thm, _)) = (case nprems_of thm of
     8.6              0 => thm
     8.7 -          | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
     8.8 +          | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!"))
     8.9    in check (Seq.pull (EVERY tacs (trivial G))) end;
    8.10  
    8.11  (*-------------------------------------------------------------*)
     9.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Oct 21 18:14:37 2005 +0200
     9.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Oct 21 18:14:38 2005 +0200
     9.3 @@ -73,7 +73,7 @@
     9.4          val induct' = refl RS ((List.nth
     9.5            (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
     9.6  
     9.7 -      in prove_goalw_cterm [] (cert t) (fn prems =>
     9.8 +      in OldGoals.prove_goalw_cterm [] (cert t) (fn prems =>
     9.9          [rtac induct' 1,
    9.10           REPEAT (rtac TrueI 1),
    9.11           REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    9.12 @@ -211,7 +211,7 @@
    9.13                THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
    9.14              descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
    9.15  
    9.16 -      in split_conj_thm (prove_goalw_cterm []
    9.17 +      in split_conj_thm (OldGoals.prove_goalw_cterm []
    9.18          (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
    9.19        end;
    9.20  
    9.21 @@ -244,7 +244,7 @@
    9.22  
    9.23      val _ = message "Proving characteristic theorems for primrec combinators ..."
    9.24  
    9.25 -    val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
    9.26 +    val rec_thms = map (fn t => OldGoals.prove_goalw_cterm reccomb_defs
    9.27        (cterm_of (Theory.sign_of thy2) t) (fn _ =>
    9.28          [rtac the1_equality 1,
    9.29           resolve_tac rec_unique_thms 1,
    9.30 @@ -318,7 +318,7 @@
    9.31          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
    9.32            (Library.take (length newTs, reccomb_names)));
    9.33  
    9.34 -    val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
    9.35 +    val case_thms = map (map (fn t => OldGoals.prove_goalw_cterm (case_defs @
    9.36        (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t)
    9.37          (fn _ => [rtac refl 1])))
    9.38            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    9.39 @@ -352,8 +352,8 @@
    9.40          val tacsf = K [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
    9.41            (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))]
    9.42        in
    9.43 -        (prove_goalw_cterm [] (cert t1) tacsf,
    9.44 -         prove_goalw_cterm [] (cert t2) tacsf)
    9.45 +        (OldGoals.prove_goalw_cterm [] (cert t1) tacsf,
    9.46 +         OldGoals.prove_goalw_cterm [] (cert t2) tacsf)
    9.47        end;
    9.48  
    9.49      val split_thm_pairs = map prove_split_thms
    9.50 @@ -419,7 +419,7 @@
    9.51  
    9.52      val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
    9.53  
    9.54 -    val size_thms = map (fn t => prove_goalw_cterm rewrites
    9.55 +    val size_thms = map (fn t => OldGoals.prove_goalw_cterm rewrites
    9.56        (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1]))
    9.57          (DatatypeProp.make_size descr sorts thy')
    9.58  
    9.59 @@ -432,7 +432,7 @@
    9.60  fun prove_weak_case_congs new_type_names descr sorts thy =
    9.61    let
    9.62      fun prove_weak_case_cong t =
    9.63 -       prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t)
    9.64 +       OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t)
    9.65           (fn prems => [rtac ((hd prems) RS arg_cong) 1])
    9.66  
    9.67      val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
    9.68 @@ -453,7 +453,7 @@
    9.69                hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
    9.70            | tac i n = rtac disjI2 i THEN tac i (n - 1)
    9.71        in 
    9.72 -        prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ =>
    9.73 +        OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ =>
    9.74            [rtac allI 1,
    9.75             exh_tac (K exhaustion) 1,
    9.76             ALLGOALS (fn i => tac i (i-1))])
    9.77 @@ -475,7 +475,7 @@
    9.78          val nchotomy'' = cterm_instantiate
    9.79            [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
    9.80        in
    9.81 -        prove_goalw_cterm [] (cert t) (fn prems => 
    9.82 +        OldGoals.prove_goalw_cterm [] (cert t) (fn prems => 
    9.83            let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
    9.84            in [simp_tac (HOL_ss addsimps [hd prems]) 1,
    9.85                cut_facts_tac [nchotomy''] 1,
    10.1 --- a/src/HOL/Tools/datatype_realizer.ML	Fri Oct 21 18:14:37 2005 +0200
    10.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Fri Oct 21 18:14:38 2005 +0200
    10.3 @@ -119,7 +119,7 @@
    10.4      val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
    10.5        (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
    10.6  
    10.7 -    val thm = simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
    10.8 +    val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
    10.9        (fn prems =>
   10.10           [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
   10.11            rtac (cterm_instantiate inst induction) 1,
   10.12 @@ -190,7 +190,7 @@
   10.13      val y = Var (("y", 0), Type.varifyT T);
   10.14      val y' = Free ("y", T);
   10.15  
   10.16 -    val thm = prove_goalw_cterm [] (cert (Logic.list_implies (prems,
   10.17 +    val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
   10.18        HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
   10.19          list_comb (r, rs @ [y'])))))
   10.20        (fn prems =>
    11.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 21 18:14:37 2005 +0200
    11.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 21 18:14:38 2005 +0200
    11.3 @@ -279,7 +279,7 @@
    11.4          val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
    11.5  
    11.6          val inj_Abs_thm = 
    11.7 -	    prove_goalw_cterm [] 
    11.8 +	    OldGoals.prove_goalw_cterm [] 
    11.9  	      (cterm_of sg
   11.10  	       (HOLogic.mk_Trueprop 
   11.11  		(Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
   11.12 @@ -289,7 +289,7 @@
   11.13          val setT = HOLogic.mk_setT T
   11.14  
   11.15          val inj_Rep_thm =
   11.16 -	    prove_goalw_cterm []
   11.17 +	    OldGoals.prove_goalw_cterm []
   11.18  	      (cterm_of sg
   11.19  	       (HOLogic.mk_Trueprop
   11.20  		(Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
   11.21 @@ -375,7 +375,7 @@
   11.22          (* prove characteristic equations *)
   11.23  
   11.24          val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
   11.25 -        val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
   11.26 +        val char_thms' = map (fn eqn => OldGoals.prove_goalw_cterm rewrites
   11.27            (cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
   11.28  
   11.29        in (thy', char_thms' @ char_thms) end;
   11.30 @@ -397,7 +397,7 @@
   11.31              val Ts = map (TFree o rpair HOLogic.typeS)
   11.32                (variantlist (replicate i "'t", used));
   11.33              val f = Free ("f", Ts ---> U)
   11.34 -          in prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
   11.35 +          in OldGoals.prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
   11.36              (HOLogic.mk_Trueprop (HOLogic.list_all
   11.37                 (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
   11.38               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
   11.39 @@ -431,7 +431,7 @@
   11.40          val inj_thms' = map (fn r => r RS injD)
   11.41            (map snd newT_iso_inj_thms @ inj_thms);
   11.42  
   11.43 -        val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
   11.44 +        val inj_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
   11.45            (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
   11.46              [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   11.47               REPEAT (EVERY
   11.48 @@ -457,7 +457,7 @@
   11.49                               (split_conj_thm inj_thm);
   11.50  
   11.51          val elem_thm = 
   11.52 -	    prove_goalw_cterm []
   11.53 +	    OldGoals.prove_goalw_cterm []
   11.54  	      (cterm_of (Theory.sign_of thy5)
   11.55  	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
   11.56  	      (fn _ =>
   11.57 @@ -495,7 +495,7 @@
   11.58  
   11.59      val iso_thms = if length descr = 1 then [] else
   11.60        Library.drop (length newTs, split_conj_thm
   11.61 -        (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
   11.62 +        (OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
   11.63             [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   11.64              REPEAT (rtac TrueI 1),
   11.65              rewrite_goals_tac (mk_meta_eq choice_eq ::
   11.66 @@ -525,7 +525,7 @@
   11.67        let
   11.68          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
   11.69          val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
   11.70 -      in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
   11.71 +      in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
   11.72          [resolve_tac inj_thms 1,
   11.73           rewrite_goals_tac rewrites,
   11.74           rtac refl 1,
   11.75 @@ -547,7 +547,7 @@
   11.76      fun prove_distinct_thms (_, []) = []
   11.77        | prove_distinct_thms (dist_rewrites', t::_::ts) =
   11.78            let
   11.79 -            val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   11.80 +            val dist_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   11.81                [simp_tac (HOL_ss addsimps dist_rewrites') 1])
   11.82            in dist_thm::(standard (dist_thm RS not_sym))::
   11.83              (prove_distinct_thms (dist_rewrites', ts))
   11.84 @@ -568,7 +568,7 @@
   11.85          ((map (fn r => r RS injD) iso_inj_thms) @
   11.86            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
   11.87             Lim_inject, Suml_inject, Sumr_inject]))
   11.88 -      in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   11.89 +      in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   11.90          [rtac iffI 1,
   11.91           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   11.92           dresolve_tac rep_congs 1, dtac box_equals 1,
   11.93 @@ -616,7 +616,7 @@
   11.94  
   11.95      val cert = cterm_of (Theory.sign_of thy6);
   11.96  
   11.97 -    val indrule_lemma = prove_goalw_cterm [] (cert
   11.98 +    val indrule_lemma = OldGoals.prove_goalw_cterm [] (cert
   11.99        (Logic.mk_implies
  11.100          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
  11.101           HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls)))) (fn prems =>
  11.102 @@ -630,7 +630,7 @@
  11.103        map (Free o apfst fst o dest_Var) Ps;
  11.104      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
  11.105  
  11.106 -    val dt_induct = prove_goalw_cterm [] (cert
  11.107 +    val dt_induct = OldGoals.prove_goalw_cterm [] (cert
  11.108        (DatatypeProp.make_ind descr sorts)) (fn prems =>
  11.109          [rtac indrule_lemma' 1,
  11.110           (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    12.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 21 18:14:37 2005 +0200
    12.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Oct 21 18:14:38 2005 +0200
    12.3 @@ -472,7 +472,7 @@
    12.4  
    12.5  fun prove_mono setT fp_fun monos thy =
    12.6   (message "  Proving monotonicity ...";
    12.7 -  Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
    12.8 +  OldGoals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
    12.9      (Thm.cterm_of thy (HOLogic.mk_Trueprop
   12.10        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   12.11      (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
   12.12 @@ -491,7 +491,7 @@
   12.13        | select_disj _ 1 = [rtac disjI1]
   12.14        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   12.15  
   12.16 -    val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   12.17 +    val intrs = map (fn (i, intr) => OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   12.18        (Thm.cterm_of thy intr) (fn prems =>
   12.19         [(*insert prems and underlying sets*)
   12.20         cut_facts_tac prems 1,
   12.21 @@ -519,7 +519,7 @@
   12.22      val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
   12.23    in
   12.24      mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
   12.25 -      quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   12.26 +      OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   12.27          (Thm.cterm_of thy t) (fn prems =>
   12.28            [cut_facts_tac [hd prems] 1,
   12.29             dtac (unfold RS subst) 1,
   12.30 @@ -648,7 +648,7 @@
   12.31      (* simplification rules for vimage and Collect *)
   12.32  
   12.33      val vimage_simps = if length cs < 2 then [] else
   12.34 -      map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
   12.35 +      map (fn c => OldGoals.quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
   12.36          (HOLogic.mk_Trueprop (HOLogic.mk_eq
   12.37            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   12.38             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   12.39 @@ -661,7 +661,7 @@
   12.40  		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
   12.41  	    else ();
   12.42  
   12.43 -    val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
   12.44 +    val induct = OldGoals.quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
   12.45        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   12.46          [rtac (impI RS allI) 1,
   12.47           DETERM (etac raw_fp_induct 1),
   12.48 @@ -676,7 +676,7 @@
   12.49           EVERY (map (fn prem =>
   12.50     	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   12.51  
   12.52 -    val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
   12.53 +    val lemma = OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
   12.54        (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   12.55          [cut_facts_tac prems 1,
   12.56           REPEAT (EVERY
    13.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Oct 21 18:14:37 2005 +0200
    13.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Oct 21 18:14:38 2005 +0200
    13.3 @@ -360,7 +360,7 @@
    13.4            (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
    13.5          val rews = map mk_meta_eq
    13.6            (fst_conv :: snd_conv :: get #rec_thms dt_info);
    13.7 -        val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
    13.8 +        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
    13.9            [if length rss = 1 then
   13.10               cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
   13.11             else EVERY [rewrite_goals_tac (rews @ all_simps),
   13.12 @@ -410,7 +410,7 @@
   13.13          val rlz = strip_all (Logic.unvarify
   13.14            (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
   13.15          val rews = map mk_meta_eq case_thms;
   13.16 -        val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   13.17 +        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   13.18            [cut_facts_tac [hd prems] 1,
   13.19             etac elimR 1,
   13.20             ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
    14.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Oct 21 18:14:37 2005 +0200
    14.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Oct 21 18:14:38 2005 +0200
    14.3 @@ -254,7 +254,7 @@
    14.4      val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
    14.5      val _ = message ("Proving equations for primrec function(s) " ^
    14.6        commas_quote (map fst nameTs1) ^ " ...");
    14.7 -    val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
    14.8 +    val simps = map (fn (_, t) => OldGoals.prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
    14.9          (fn _ => [rtac refl 1])) eqns;
   14.10      val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
   14.11      val thy''' = thy''
    15.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Oct 21 18:14:37 2005 +0200
    15.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Oct 21 18:14:38 2005 +0200
    15.3 @@ -130,7 +130,7 @@
    15.4      let val tm = elimR2Fol th
    15.5  	val ctm = cterm_of (sign_of_thm th) tm	
    15.6      in
    15.7 -	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
    15.8 +	OldGoals.prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
    15.9      end
   15.10   else th;
   15.11  
   15.12 @@ -240,7 +240,7 @@
   15.13        val cex = Thm.cterm_of sign (HOLogic.exists_const T)
   15.14        val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
   15.15        and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
   15.16 -  in  prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc))
   15.17 +  in  OldGoals.prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc))
   15.18  	    (fn [prem] => [ rtac (prem RS someI_ex) 1 ])
   15.19    end;	 
   15.20  
    16.1 --- a/src/HOL/arith_data.ML	Fri Oct 21 18:14:37 2005 +0200
    16.2 +++ b/src/HOL/arith_data.ML	Fri Oct 21 18:14:38 2005 +0200
    16.3 @@ -52,7 +52,7 @@
    16.4  val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    16.5  
    16.6  fun prove_conv expand_tac norm_tac sg ss tu =
    16.7 -  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
    16.8 +  mk_meta_eq (OldGoals.prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
    16.9      (K [expand_tac, norm_tac ss]))
   16.10    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   16.11      (string_of_cterm (cterm_of sg (mk_eqv tu))));
    17.1 --- a/src/HOL/simpdata.ML	Fri Oct 21 18:14:37 2005 +0200
    17.2 +++ b/src/HOL/simpdata.ML	Fri Oct 21 18:14:38 2005 +0200
    17.3 @@ -253,7 +253,7 @@
    17.4          val aT = TFree ("'a", HOLogic.typeS);
    17.5          val x = Free ("x", aT);
    17.6          val y = Free ("y", aT)
    17.7 -      in prove_goalw_cterm [simp_implies_def]
    17.8 +      in OldGoals.prove_goalw_cterm [simp_implies_def]
    17.9          (cterm_of sign (Logic.mk_implies
   17.10            (mk_simp_implies (Logic.mk_equals (x, y)),
   17.11             mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))))
    18.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Fri Oct 21 18:14:37 2005 +0200
    18.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Fri Oct 21 18:14:38 2005 +0200
    18.3 @@ -226,7 +226,7 @@
    18.4  structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
    18.5  in
    18.6  (
    18.7 -push_proof();
    18.8 +OldGoals.push_proof();
    18.9  Goal 
   18.10  ( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
   18.11    "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
   18.12 @@ -271,7 +271,7 @@
   18.13  (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
   18.14  by (atac 1);
   18.15  result();
   18.16 -pop_proof();
   18.17 +OldGoals.pop_proof();
   18.18  Logic.strip_imp_concl subgoal
   18.19  )
   18.20  end)
    19.1 --- a/src/HOLCF/domain/theorems.ML	Fri Oct 21 18:14:37 2005 +0200
    19.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Oct 21 18:14:38 2005 +0200
    19.3 @@ -24,7 +24,7 @@
    19.4  
    19.5  fun pg'' thy defs t = let val sg = sign_of thy;
    19.6                            val ct = Thm.cterm_of sg (inferT sg t);
    19.7 -                      in prove_goalw_cterm defs ct end;
    19.8 +                      in OldGoals.prove_goalw_cterm defs ct end;
    19.9  fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf 
   19.10                                  | prems=> (cut_facts_tac prems 1)::tacsf);
   19.11  
    20.1 --- a/src/HOLCF/fixrec_package.ML	Fri Oct 21 18:14:37 2005 +0200
    20.2 +++ b/src/HOLCF/fixrec_package.ML	Fri Oct 21 18:14:38 2005 +0200
    20.3 @@ -107,7 +107,7 @@
    20.4      
    20.5      fun mk_cterm t = cterm_of thy' (infer thy' t);
    20.6      val ctuple_unfold_ct = mk_cterm (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
    20.7 -    val ctuple_unfold_thm = prove_goalw_cterm [] ctuple_unfold_ct
    20.8 +    val ctuple_unfold_thm = OldGoals.prove_goalw_cterm [] ctuple_unfold_ct
    20.9            (fn _ => [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
   20.10                      simp_tac (simpset_of thy') 1]);
   20.11      val ctuple_induct_thm =
   20.12 @@ -218,7 +218,7 @@
   20.13    let
   20.14      fun tacsf prems =
   20.15        [rtac (unfold_thm RS ssubst_lhs) 1, simp_tac (simpset_of thy addsimps prems) 1];
   20.16 -    fun prove_term t = prove_goalw_cterm [] (cterm_of thy t) tacsf;
   20.17 +    fun prove_term t = OldGoals.prove_goalw_cterm [] (cterm_of thy t) tacsf;
   20.18      fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
   20.19    in
   20.20      map prove_eqn eqns
   20.21 @@ -275,7 +275,7 @@
   20.22      val cname = case chead_of t of Const(c,_) => c | _ =>
   20.23                fixrec_err "function is not declared as constant in theory";
   20.24      val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
   20.25 -    val simp = prove_goalw_cterm [] (cterm_of thy eq)
   20.26 +    val simp = OldGoals.prove_goalw_cterm [] (cterm_of thy eq)
   20.27            (fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   20.28    in simp end;
   20.29  
    21.1 --- a/src/Provers/splitter.ML	Fri Oct 21 18:14:37 2005 +0200
    21.2 +++ b/src/Provers/splitter.ML	Fri Oct 21 18:14:38 2005 +0200
    21.3 @@ -73,7 +73,7 @@
    21.4    let val ct = read_cterm (#sign(rep_thm Data.iffD))
    21.5             ("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \
    21.6              \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
    21.7 -  in prove_goalw_cterm [] ct
    21.8 +  in OldGoals.prove_goalw_cterm [] ct
    21.9       (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
   21.10    end;
   21.11  
    22.1 --- a/src/Pure/proof_general.ML	Fri Oct 21 18:14:37 2005 +0200
    22.2 +++ b/src/Pure/proof_general.ML	Fri Oct 21 18:14:38 2005 +0200
    22.3 @@ -370,7 +370,7 @@
    22.4  val help = welcome;
    22.5  val show_context = Context.the_context;
    22.6  
    22.7 -fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
    22.8 +fun kill_goal () = (OldGoals.reset_goals (); tell_clear_goals ());
    22.9  
   22.10  fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
   22.11  
    23.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Oct 21 18:14:37 2005 +0200
    23.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Oct 21 18:14:38 2005 +0200
    23.3 @@ -279,7 +279,7 @@
    23.4                            Su.case_inr RS trans] 1)];
    23.5  
    23.6    fun prove_case_eqn (arg,con_def) =
    23.7 -      prove_goalw_cterm []
    23.8 +      OldGoals.prove_goalw_cterm []
    23.9          (Ind_Syntax.traceIt "next case equation = "
   23.10             (cterm_of (sign_of thy1) (mk_case_eqn arg)))
   23.11          (case_tacsf con_def);
   23.12 @@ -324,7 +324,7 @@
   23.13             IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];
   23.14  
   23.15          fun prove_recursor_eqn arg =
   23.16 -            prove_goalw_cterm []
   23.17 +            OldGoals.prove_goalw_cterm []
   23.18                (Ind_Syntax.traceIt "next recursor equation = "
   23.19                  (cterm_of (sign_of thy1) (mk_recursor_eqn arg)))
   23.20                recursor_tacsf
   23.21 @@ -342,7 +342,7 @@
   23.22    (*Typical theorems have the form ~con1=con2, con1=con2==>False,
   23.23      con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
   23.24    fun mk_free s =
   23.25 -      prove_goalw (theory_of_thm elim)   (*Don't use thy1: it will be stale*)
   23.26 +      OldGoals.prove_goalw (theory_of_thm elim)   (*Don't use thy1: it will be stale*)
   23.27                    con_defs s
   23.28          (fn prems => [cut_facts_tac prems 1,
   23.29                        fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]);
    24.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Oct 21 18:14:37 2005 +0200
    24.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Oct 21 18:14:38 2005 +0200
    24.3 @@ -192,7 +192,7 @@
    24.4    val dummy = writeln "  Proving monotonicity...";
    24.5  
    24.6    val bnd_mono =
    24.7 -      prove_goalw_cterm []
    24.8 +      OldGoals.prove_goalw_cterm []
    24.9          (cterm_of sign1
   24.10                    (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
   24.11          (fn _ =>
   24.12 @@ -251,7 +251,7 @@
   24.13            and g rl = rl RS disjI2
   24.14        in  accesses_bal(f, g, asm_rl)  end;
   24.15  
   24.16 -  fun prove_intr (ct, tacsf) = prove_goalw_cterm part_rec_defs ct tacsf;
   24.17 +  fun prove_intr (ct, tacsf) = OldGoals.prove_goalw_cterm part_rec_defs ct tacsf;
   24.18  
   24.19    val intrs = ListPair.map prove_intr
   24.20                  (map (cterm_of sign1) intr_tms,
   24.21 @@ -345,7 +345,7 @@
   24.22                                     ORELSE' etac FalseE));
   24.23  
   24.24       val quant_induct =
   24.25 -         prove_goalw_cterm part_rec_defs
   24.26 +         OldGoals.prove_goalw_cterm part_rec_defs
   24.27             (cterm_of sign1
   24.28              (Logic.list_implies
   24.29               (ind_prems,
   24.30 @@ -431,7 +431,7 @@
   24.31       val lemma = (*makes the link between the two induction rules*)
   24.32         if need_mutual then
   24.33            (writeln "  Proving the mutual induction rule...";
   24.34 -           prove_goalw_cterm part_rec_defs
   24.35 +           OldGoals.prove_goalw_cterm part_rec_defs
   24.36                   (cterm_of sign1 (Logic.mk_implies (induct_concl,
   24.37                                                     mutual_induct_concl)))
   24.38                   (fn prems =>
   24.39 @@ -493,7 +493,7 @@
   24.40  
   24.41       val mutual_induct_fsplit =
   24.42         if need_mutual then
   24.43 -         prove_goalw_cterm []
   24.44 +         OldGoals.prove_goalw_cterm []
   24.45                 (cterm_of sign1
   24.46                  (Logic.list_implies
   24.47                     (map (induct_prem (rec_tms~~preds)) intr_tms,
    25.1 --- a/src/ZF/Tools/primrec_package.ML	Fri Oct 21 18:14:37 2005 +0200
    25.2 +++ b/src/ZF/Tools/primrec_package.ML	Fri Oct 21 18:14:38 2005 +0200
    25.3 @@ -182,7 +182,7 @@
    25.4      val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
    25.5      val eqn_thms =
    25.6        (message ("Proving equations for primrec function " ^ fname);
    25.7 -      map (fn t => prove_goalw_cterm rewrites
    25.8 +      map (fn t => OldGoals.prove_goalw_cterm rewrites
    25.9          (Ind_Syntax.traceIt "next primrec equation = " (cterm_of (sign_of thy1) t))
   25.10          (fn _ => [rtac refl 1])) eqn_terms);
   25.11