avoid legacy goals;
authorwenzelm
Tue Oct 25 18:18:49 2005 +0200 (2005-10-25)
changeset 17985d5d576b72371
parent 17984 bdac047db2a5
child 17986 0450847646c3
avoid legacy goals;
TFL/rules.ML
src/HOL/Hyperreal/transfer.ML
src/HOL/Integ/cooper_proof.ML
src/HOL/Tools/Presburger/cooper_proof.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/arith_data.ML
src/HOL/simpdata.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/fixrec_package.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/TFL/rules.ML	Sat Oct 22 01:22:10 2005 +0200
     1.2 +++ b/TFL/rules.ML	Tue Oct 25 18:18:49 2005 +0200
     1.3 @@ -814,13 +814,12 @@
     1.4  
     1.5  
     1.6  fun prove strict (ptm, tac) =
     1.7 -  let val result =
     1.8 -    if strict then OldGoals.prove_goalw_cterm [] ptm (fn _ => [tac])
     1.9 -    else
    1.10 -      transform_error (fn () =>
    1.11 -        OldGoals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
    1.12 -      handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
    1.13 -  in #1 (freeze_thaw result) end;
    1.14 -
    1.15 +  let
    1.16 +    val {thy, t, ...} = Thm.rep_cterm ptm;
    1.17 +    val result =
    1.18 +      if strict then Goal.prove thy [] [] t (K tac)
    1.19 +      else Goal.prove thy [] [] t (K tac)
    1.20 +        handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
    1.21 +  in #1 (freeze_thaw (standard result)) end;
    1.22  
    1.23  end;
     2.1 --- a/src/HOL/Hyperreal/transfer.ML	Sat Oct 22 01:22:10 2005 +0200
     2.2 +++ b/src/HOL/Hyperreal/transfer.ML	Tue Oct 25 18:18:49 2005 +0200
     2.3 @@ -64,16 +64,14 @@
     2.4      val {intros,unfolds,refolds,consts} = TransferData.get thy
     2.5      val (_$_$t') = concl_of (Tactic.rewrite true unfolds (cterm_of thy t))
     2.6      val u = unstar_term consts t'
     2.7 -    val ct = cterm_of thy (Logic.mk_equals (t,u))
     2.8      val tacs =
     2.9 -      [ rewrite_goals_tac atomizers
    2.10 +      [ rewrite_goals_tac (ths @ refolds @ unfolds)
    2.11 +      , rewrite_goals_tac atomizers
    2.12        , match_tac [transitive_thm] 1
    2.13        , resolve_tac [transfer_start] 1
    2.14        , REPEAT_ALL_NEW (resolve_tac intros) 1
    2.15        , match_tac [reflexive_thm] 1 ]
    2.16 -  in
    2.17 -    OldGoals.prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
    2.18 -  end
    2.19 +  in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (fn _ => EVERY tacs) end
    2.20  
    2.21  fun transfer_tac ths =
    2.22      SUBGOAL (fn (t,i) =>
     3.1 --- a/src/HOL/Integ/cooper_proof.ML	Sat Oct 22 01:22:10 2005 +0200
     3.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Oct 25 18:18:49 2005 +0200
     3.3 @@ -189,47 +189,21 @@
     3.4  fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
     3.5  
     3.6  (* ------------------------------------------------------------------------- *)
     3.7 -(* Modified version of the simple version with minimal amount of checking and postprocessing*)
     3.8 +(*This function proove elementar will be used to generate proofs at
     3.9 +  runtime*) (*It is thought to prove properties such as a dvd b
    3.10 +  (essentially) that are only to make at runtime.*)
    3.11  (* ------------------------------------------------------------------------- *)
    3.12 -
    3.13 -fun simple_prove_goal_cterm2 G tacs =
    3.14 -  let
    3.15 -    fun check NONE = error "prove_goal: tactic failed"
    3.16 -      | check (SOME (thm, _)) = (case nprems_of thm of
    3.17 -            0 => thm
    3.18 -          | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!"))
    3.19 -  in check (Seq.pull (EVERY tacs (trivial G))) end;
    3.20 -
    3.21 -(*-------------------------------------------------------------*)
    3.22 -(*-------------------------------------------------------------*)
    3.23 -
    3.24 -fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
    3.25 -
    3.26 -(* ------------------------------------------------------------------------- *)
    3.27 -(*This function proove elementar will be used to generate proofs at runtime*)
    3.28 -(*It is is based on the isabelle function proove_goalw_cterm and is thought to *)
    3.29 -(*prove properties such as a dvd b (essentially) that are only to make at
    3.30 -runtime.*)
    3.31 -(* ------------------------------------------------------------------------- *)
    3.32 -fun prove_elementar sg s fm2 = case s of 
    3.33 +fun prove_elementar thy s fm2 =
    3.34 +  Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
    3.35 +  (case s of
    3.36    (*"ss" like simplification with simpset*)
    3.37    "ss" =>
    3.38 -    let
    3.39 -      val ss = presburger_ss addsimps
    3.40 -        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
    3.41 -      val ct =  cert_Trueprop sg fm2
    3.42 -    in 
    3.43 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] 
    3.44 -
    3.45 -    end
    3.46 +    let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex]
    3.47 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end
    3.48  
    3.49    (*"bl" like blast tactic*)
    3.50    (* Is only used in the harrisons like proof procedure *)
    3.51 -  | "bl" =>
    3.52 -     let val ct = cert_Trueprop sg fm2
    3.53 -     in
    3.54 -       simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1]
    3.55 -     end
    3.56 +  | "bl" => [blast_tac HOL_cs 1]
    3.57  
    3.58    (*"ed" like Existence disjunctions ...*)
    3.59    (* Is only used in the harrisons like proof procedure *)
    3.60 @@ -244,51 +218,26 @@
    3.61            etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1,
    3.62            REPEAT(EVERY[etac disjE 1, tac2]), tac2]
    3.63          end
    3.64 -
    3.65 -      val ct = cert_Trueprop sg fm2
    3.66 -    in 
    3.67 -      simple_prove_goal_cterm2 ct ex_disj_tacs
    3.68 -    end
    3.69 +    in ex_disj_tacs end
    3.70  
    3.71 -  | "fa" =>
    3.72 -    let val ct = cert_Trueprop sg fm2
    3.73 -    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]  
    3.74 -
    3.75 -    end
    3.76 +  | "fa" => [simple_arith_tac 1]
    3.77  
    3.78    | "sa" =>
    3.79 -    let
    3.80 -      val ss = presburger_ss addsimps zadd_ac
    3.81 -      val ct = cert_Trueprop sg fm2
    3.82 -    in 
    3.83 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    3.84 +    let val ss = presburger_ss addsimps zadd_ac
    3.85 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end
    3.86  
    3.87 -    end
    3.88    (* like Existance Conjunction *)
    3.89    | "ec" =>
    3.90 -    let
    3.91 -      val ss = presburger_ss addsimps zadd_ac
    3.92 -      val ct = cert_Trueprop sg fm2
    3.93 -    in 
    3.94 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)]
    3.95 -    end
    3.96 +    let val ss = presburger_ss addsimps zadd_ac
    3.97 +    in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end
    3.98  
    3.99    | "ac" =>
   3.100 -    let
   3.101 -      val ss = HOL_basic_ss addsimps zadd_ac
   3.102 -      val ct = cert_Trueprop sg fm2
   3.103 -    in 
   3.104 -      simple_prove_goal_cterm2 ct [simp_tac ss 1]
   3.105 -    end
   3.106 +    let val ss = HOL_basic_ss addsimps zadd_ac
   3.107 +    in [simp_tac ss 1] end
   3.108  
   3.109    | "lf" =>
   3.110 -    let
   3.111 -      val ss = presburger_ss addsimps zadd_ac
   3.112 -      val ct = cert_Trueprop sg fm2
   3.113 -    in 
   3.114 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
   3.115 -
   3.116 -    end;
   3.117 +    let val ss = presburger_ss addsimps zadd_ac
   3.118 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end));
   3.119  
   3.120  (*=============================================================*)
   3.121  (*-------------------------------------------------------------*)
     4.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Oct 22 01:22:10 2005 +0200
     4.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Oct 25 18:18:49 2005 +0200
     4.3 @@ -189,47 +189,21 @@
     4.4  fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
     4.5  
     4.6  (* ------------------------------------------------------------------------- *)
     4.7 -(* Modified version of the simple version with minimal amount of checking and postprocessing*)
     4.8 +(*This function proove elementar will be used to generate proofs at
     4.9 +  runtime*) (*It is thought to prove properties such as a dvd b
    4.10 +  (essentially) that are only to make at runtime.*)
    4.11  (* ------------------------------------------------------------------------- *)
    4.12 -
    4.13 -fun simple_prove_goal_cterm2 G tacs =
    4.14 -  let
    4.15 -    fun check NONE = error "prove_goal: tactic failed"
    4.16 -      | check (SOME (thm, _)) = (case nprems_of thm of
    4.17 -            0 => thm
    4.18 -          | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!"))
    4.19 -  in check (Seq.pull (EVERY tacs (trivial G))) end;
    4.20 -
    4.21 -(*-------------------------------------------------------------*)
    4.22 -(*-------------------------------------------------------------*)
    4.23 -
    4.24 -fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
    4.25 -
    4.26 -(* ------------------------------------------------------------------------- *)
    4.27 -(*This function proove elementar will be used to generate proofs at runtime*)
    4.28 -(*It is is based on the isabelle function proove_goalw_cterm and is thought to *)
    4.29 -(*prove properties such as a dvd b (essentially) that are only to make at
    4.30 -runtime.*)
    4.31 -(* ------------------------------------------------------------------------- *)
    4.32 -fun prove_elementar sg s fm2 = case s of 
    4.33 +fun prove_elementar thy s fm2 =
    4.34 +  Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
    4.35 +  (case s of
    4.36    (*"ss" like simplification with simpset*)
    4.37    "ss" =>
    4.38 -    let
    4.39 -      val ss = presburger_ss addsimps
    4.40 -        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
    4.41 -      val ct =  cert_Trueprop sg fm2
    4.42 -    in 
    4.43 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] 
    4.44 -
    4.45 -    end
    4.46 +    let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex]
    4.47 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end
    4.48  
    4.49    (*"bl" like blast tactic*)
    4.50    (* Is only used in the harrisons like proof procedure *)
    4.51 -  | "bl" =>
    4.52 -     let val ct = cert_Trueprop sg fm2
    4.53 -     in
    4.54 -       simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1]
    4.55 -     end
    4.56 +  | "bl" => [blast_tac HOL_cs 1]
    4.57  
    4.58    (*"ed" like Existence disjunctions ...*)
    4.59    (* Is only used in the harrisons like proof procedure *)
    4.60 @@ -244,51 +218,26 @@
    4.61            etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1,
    4.62            REPEAT(EVERY[etac disjE 1, tac2]), tac2]
    4.63          end
    4.64 -
    4.65 -      val ct = cert_Trueprop sg fm2
    4.66 -    in 
    4.67 -      simple_prove_goal_cterm2 ct ex_disj_tacs
    4.68 -    end
    4.69 +    in ex_disj_tacs end
    4.70  
    4.71 -  | "fa" =>
    4.72 -    let val ct = cert_Trueprop sg fm2
    4.73 -    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]  
    4.74 -
    4.75 -    end
    4.76 +  | "fa" => [simple_arith_tac 1]
    4.77  
    4.78    | "sa" =>
    4.79 -    let
    4.80 -      val ss = presburger_ss addsimps zadd_ac
    4.81 -      val ct = cert_Trueprop sg fm2
    4.82 -    in 
    4.83 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    4.84 +    let val ss = presburger_ss addsimps zadd_ac
    4.85 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end
    4.86  
    4.87 -    end
    4.88    (* like Existance Conjunction *)
    4.89    | "ec" =>
    4.90 -    let
    4.91 -      val ss = presburger_ss addsimps zadd_ac
    4.92 -      val ct = cert_Trueprop sg fm2
    4.93 -    in 
    4.94 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)]
    4.95 -    end
    4.96 +    let val ss = presburger_ss addsimps zadd_ac
    4.97 +    in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end
    4.98  
    4.99    | "ac" =>
   4.100 -    let
   4.101 -      val ss = HOL_basic_ss addsimps zadd_ac
   4.102 -      val ct = cert_Trueprop sg fm2
   4.103 -    in 
   4.104 -      simple_prove_goal_cterm2 ct [simp_tac ss 1]
   4.105 -    end
   4.106 +    let val ss = HOL_basic_ss addsimps zadd_ac
   4.107 +    in [simp_tac ss 1] end
   4.108  
   4.109    | "lf" =>
   4.110 -    let
   4.111 -      val ss = presburger_ss addsimps zadd_ac
   4.112 -      val ct = cert_Trueprop sg fm2
   4.113 -    in 
   4.114 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
   4.115 -
   4.116 -    end;
   4.117 +    let val ss = presburger_ss addsimps zadd_ac
   4.118 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end));
   4.119  
   4.120  (*=============================================================*)
   4.121  (*-------------------------------------------------------------*)
     5.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Oct 22 01:22:10 2005 +0200
     5.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Oct 25 18:18:49 2005 +0200
     5.3 @@ -68,16 +68,18 @@
     5.4          val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
     5.5            Var (("P", 0), HOLogic.boolT))
     5.6          val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
     5.7 -        val cert = cterm_of (Theory.sign_of thy);
     5.8 +        val cert = cterm_of thy;
     5.9          val insts' = (map cert induct_Ps) ~~ (map cert insts);
    5.10          val induct' = refl RS ((List.nth
    5.11            (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
    5.12  
    5.13 -      in OldGoals.prove_goalw_cterm [] (cert t) (fn prems =>
    5.14 -        [rtac induct' 1,
    5.15 -         REPEAT (rtac TrueI 1),
    5.16 -         REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    5.17 -         REPEAT (rtac TrueI 1)])
    5.18 +      in
    5.19 +        standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    5.20 +          (fn prems => EVERY
    5.21 +            [rtac induct' 1,
    5.22 +             REPEAT (rtac TrueI 1),
    5.23 +             REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    5.24 +             REPEAT (rtac TrueI 1)]))
    5.25        end;
    5.26  
    5.27      val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
    5.28 @@ -201,7 +203,7 @@
    5.29              absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod
    5.30                (mk_Free "x" T1 i, Free ("y", T2)), set_t)))
    5.31                  (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
    5.32 -        val cert = cterm_of (Theory.sign_of thy1)
    5.33 +        val cert = cterm_of thy1
    5.34          val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
    5.35            ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
    5.36          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
    5.37 @@ -211,8 +213,8 @@
    5.38                THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
    5.39              descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
    5.40  
    5.41 -      in split_conj_thm (OldGoals.prove_goalw_cterm []
    5.42 -        (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
    5.43 +      in split_conj_thm (standard (Goal.prove thy1 [] []
    5.44 +        (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac)))
    5.45        end;
    5.46  
    5.47      val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
    5.48 @@ -244,12 +246,13 @@
    5.49  
    5.50      val _ = message "Proving characteristic theorems for primrec combinators ..."
    5.51  
    5.52 -    val rec_thms = map (fn t => OldGoals.prove_goalw_cterm reccomb_defs
    5.53 -      (cterm_of (Theory.sign_of thy2) t) (fn _ =>
    5.54 -        [rtac the1_equality 1,
    5.55 +    val rec_thms = map (fn t => standard (Goal.prove thy2 [] [] t
    5.56 +      (fn _ => EVERY
    5.57 +        [rewrite_goals_tac reccomb_defs,
    5.58 +         rtac the1_equality 1,
    5.59           resolve_tac rec_unique_thms 1,
    5.60           resolve_tac rec_intrs 1,
    5.61 -         REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
    5.62 +         REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)])))
    5.63             (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
    5.64  
    5.65    in
    5.66 @@ -318,9 +321,8 @@
    5.67          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
    5.68            (Library.take (length newTs, reccomb_names)));
    5.69  
    5.70 -    val case_thms = map (map (fn t => OldGoals.prove_goalw_cterm (case_defs @
    5.71 -      (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t)
    5.72 -        (fn _ => [rtac refl 1])))
    5.73 +    val case_thms = map (map (fn t => standard (Goal.prove thy2 [] [] t
    5.74 +      (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))))
    5.75            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    5.76  
    5.77    in
    5.78 @@ -345,15 +347,15 @@
    5.79      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
    5.80          exhaustion), case_thms'), T) =
    5.81        let
    5.82 -        val cert = cterm_of (Theory.sign_of thy);
    5.83 +        val cert = cterm_of thy;
    5.84          val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
    5.85          val exhaustion' = cterm_instantiate
    5.86            [(cert lhs, cert (Free ("x", T)))] exhaustion;
    5.87 -        val tacsf = K [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
    5.88 -          (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))]
    5.89 +        val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
    5.90 +          (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
    5.91        in
    5.92 -        (OldGoals.prove_goalw_cterm [] (cert t1) tacsf,
    5.93 -         OldGoals.prove_goalw_cterm [] (cert t2) tacsf)
    5.94 +        (standard (Goal.prove thy [] [] t1 tacf),
    5.95 +         standard (Goal.prove thy [] [] t2 tacf))
    5.96        end;
    5.97  
    5.98      val split_thm_pairs = map prove_split_thms
    5.99 @@ -419,8 +421,8 @@
   5.100  
   5.101      val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
   5.102  
   5.103 -    val size_thms = map (fn t => OldGoals.prove_goalw_cterm rewrites
   5.104 -      (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1]))
   5.105 +    val size_thms = map (fn t => standard (Goal.prove thy' [] [] t
   5.106 +      (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])))
   5.107          (DatatypeProp.make_size descr sorts thy')
   5.108  
   5.109    in
   5.110 @@ -432,8 +434,8 @@
   5.111  fun prove_weak_case_congs new_type_names descr sorts thy =
   5.112    let
   5.113      fun prove_weak_case_cong t =
   5.114 -       OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t)
   5.115 -         (fn prems => [rtac ((hd prems) RS arg_cong) 1])
   5.116 +       standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   5.117 +         (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1]))
   5.118  
   5.119      val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
   5.120        new_type_names descr sorts thy)
   5.121 @@ -453,10 +455,10 @@
   5.122                hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
   5.123            | tac i n = rtac disjI2 i THEN tac i (n - 1)
   5.124        in 
   5.125 -        OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ =>
   5.126 -          [rtac allI 1,
   5.127 +        standard (Goal.prove thy [] [] t (fn _ =>
   5.128 +          EVERY [rtac allI 1,
   5.129             exh_tac (K exhaustion) 1,
   5.130 -           ALLGOALS (fn i => tac i (i-1))])
   5.131 +           ALLGOALS (fn i => tac i (i-1))]))
   5.132        end;
   5.133  
   5.134      val nchotomys =
   5.135 @@ -475,13 +477,14 @@
   5.136          val nchotomy'' = cterm_instantiate
   5.137            [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
   5.138        in
   5.139 -        OldGoals.prove_goalw_cterm [] (cert t) (fn prems => 
   5.140 -          let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
   5.141 -          in [simp_tac (HOL_ss addsimps [hd prems]) 1,
   5.142 -              cut_facts_tac [nchotomy''] 1,
   5.143 -              REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
   5.144 -              REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
   5.145 -          end)
   5.146 +        standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   5.147 +          (fn prems => 
   5.148 +            let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
   5.149 +            in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
   5.150 +                cut_facts_tac [nchotomy''] 1,
   5.151 +                REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
   5.152 +                REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
   5.153 +            end))
   5.154        end;
   5.155  
   5.156      val case_congs = map prove_case_cong (DatatypeProp.make_case_congs
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sat Oct 22 01:22:10 2005 +0200
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 25 18:18:49 2005 +0200
     6.3 @@ -279,22 +279,20 @@
     6.4          val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
     6.5  
     6.6          val inj_Abs_thm = 
     6.7 -	    OldGoals.prove_goalw_cterm [] 
     6.8 -	      (cterm_of sg
     6.9 -	       (HOLogic.mk_Trueprop 
    6.10 +	    standard (Goal.prove sg [] []
    6.11 +	      (HOLogic.mk_Trueprop 
    6.12  		(Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
    6.13 -		 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))))
    6.14 -              (fn _ => [rtac inj_on_inverseI 1, etac thm1 1]);
    6.15 +		 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))
    6.16 +              (fn _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1]));
    6.17  
    6.18          val setT = HOLogic.mk_setT T
    6.19  
    6.20          val inj_Rep_thm =
    6.21 -	    OldGoals.prove_goalw_cterm []
    6.22 -	      (cterm_of sg
    6.23 -	       (HOLogic.mk_Trueprop
    6.24 +	    standard (Goal.prove sg [] []
    6.25 +	      (HOLogic.mk_Trueprop
    6.26  		(Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
    6.27 -		 Const (Rep_name, RepT) $ Const ("UNIV", setT))))
    6.28 -              (fn _ => [rtac inj_inverseI 1, rtac thm2 1])
    6.29 +		 Const (Rep_name, RepT) $ Const ("UNIV", setT)))
    6.30 +              (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1]));
    6.31  
    6.32        in (inj_Abs_thm, inj_Rep_thm) end;
    6.33  
    6.34 @@ -375,8 +373,8 @@
    6.35          (* prove characteristic equations *)
    6.36  
    6.37          val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
    6.38 -        val char_thms' = map (fn eqn => OldGoals.prove_goalw_cterm rewrites
    6.39 -          (cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
    6.40 +        val char_thms' = map (fn eqn => standard (Goal.prove thy' [] [] eqn
    6.41 +          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
    6.42  
    6.43        in (thy', char_thms' @ char_thms) end;
    6.44  
    6.45 @@ -397,13 +395,12 @@
    6.46              val Ts = map (TFree o rpair HOLogic.typeS)
    6.47                (variantlist (replicate i "'t", used));
    6.48              val f = Free ("f", Ts ---> U)
    6.49 -          in OldGoals.prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
    6.50 +          in standard (Goal.prove sign [] [] (Logic.mk_implies
    6.51              (HOLogic.mk_Trueprop (HOLogic.list_all
    6.52                 (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
    6.53               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
    6.54 -               r $ (a $ app_bnds f i)), f))))) (fn prems =>
    6.55 -                 [cut_facts_tac prems 1, REPEAT (rtac ext 1),
    6.56 -                  REPEAT (etac allE 1), rtac thm 1, atac 1])
    6.57 +               r $ (a $ app_bnds f i)), f))))
    6.58 +            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1]))
    6.59            end
    6.60        in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
    6.61  
    6.62 @@ -431,8 +428,8 @@
    6.63          val inj_thms' = map (fn r => r RS injD)
    6.64            (map snd newT_iso_inj_thms @ inj_thms);
    6.65  
    6.66 -        val inj_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
    6.67 -          (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
    6.68 +        val inj_thm = standard (Goal.prove thy5 [] []
    6.69 +          (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    6.70              [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    6.71               REPEAT (EVERY
    6.72                 [rtac allI 1, rtac impI 1,
    6.73 @@ -451,20 +448,18 @@
    6.74                           REPEAT (eresolve_tac (mp :: allE ::
    6.75                             map make_elim (Suml_inject :: Sumr_inject ::
    6.76                               Lim_inject :: fun_cong :: inj_thms')) 1),
    6.77 -                         atac 1]))])])])]);
    6.78 +                         atac 1]))])])])]));
    6.79  
    6.80          val inj_thms'' = map (fn r => r RS datatype_injI)
    6.81                               (split_conj_thm inj_thm);
    6.82  
    6.83          val elem_thm = 
    6.84 -	    OldGoals.prove_goalw_cterm []
    6.85 -	      (cterm_of (Theory.sign_of thy5)
    6.86 -	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
    6.87 +	    standard (Goal.prove thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    6.88  	      (fn _ =>
    6.89 -	       [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    6.90 +	       EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    6.91  		rewrite_goals_tac rewrites,
    6.92  		REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    6.93 -                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
    6.94 +                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]));
    6.95  
    6.96        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
    6.97        end;
    6.98 @@ -495,7 +490,7 @@
    6.99  
   6.100      val iso_thms = if length descr = 1 then [] else
   6.101        Library.drop (length newTs, split_conj_thm
   6.102 -        (OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
   6.103 +        (standard (Goal.prove thy5 [] [] iso_t (fn _ => EVERY
   6.104             [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   6.105              REPEAT (rtac TrueI 1),
   6.106              rewrite_goals_tac (mk_meta_eq choice_eq ::
   6.107 @@ -506,7 +501,7 @@
   6.108                   List.concat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
   6.109                 TRY (hyp_subst_tac 1),
   6.110                 rtac (sym RS range_eqI) 1,
   6.111 -               resolve_tac iso_char_thms 1])])));
   6.112 +               resolve_tac iso_char_thms 1])]))));
   6.113  
   6.114      val Abs_inverse_thms' =
   6.115        map #1 newT_iso_axms @
   6.116 @@ -525,12 +520,12 @@
   6.117        let
   6.118          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
   6.119          val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
   6.120 -      in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
   6.121 +      in standard (Goal.prove thy5 [] [] eqn (fn _ => EVERY
   6.122          [resolve_tac inj_thms 1,
   6.123           rewrite_goals_tac rewrites,
   6.124           rtac refl 1,
   6.125           resolve_tac rep_intrs 2,
   6.126 -         REPEAT (resolve_tac iso_elem_thms 1)])
   6.127 +         REPEAT (resolve_tac iso_elem_thms 1)]))
   6.128        end;
   6.129  
   6.130      (*--------------------------------------------------------------*)
   6.131 @@ -547,8 +542,8 @@
   6.132      fun prove_distinct_thms (_, []) = []
   6.133        | prove_distinct_thms (dist_rewrites', t::_::ts) =
   6.134            let
   6.135 -            val dist_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   6.136 -              [simp_tac (HOL_ss addsimps dist_rewrites') 1])
   6.137 +            val dist_thm = standard (Goal.prove thy5 [] [] t (fn _ =>
   6.138 +              EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]))
   6.139            in dist_thm::(standard (dist_thm RS not_sym))::
   6.140              (prove_distinct_thms (dist_rewrites', ts))
   6.141            end;
   6.142 @@ -568,7 +563,7 @@
   6.143          ((map (fn r => r RS injD) iso_inj_thms) @
   6.144            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
   6.145             Lim_inject, Suml_inject, Sumr_inject]))
   6.146 -      in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   6.147 +      in standard (Goal.prove thy5 [] [] t (fn _ => EVERY
   6.148          [rtac iffI 1,
   6.149           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   6.150           dresolve_tac rep_congs 1, dtac box_equals 1,
   6.151 @@ -576,7 +571,7 @@
   6.152           REPEAT (eresolve_tac inj_thms 1),
   6.153           REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
   6.154             REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
   6.155 -           atac 1]))])
   6.156 +           atac 1]))]))
   6.157        end;
   6.158  
   6.159      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   6.160 @@ -616,29 +611,31 @@
   6.161  
   6.162      val cert = cterm_of (Theory.sign_of thy6);
   6.163  
   6.164 -    val indrule_lemma = OldGoals.prove_goalw_cterm [] (cert
   6.165 +    val indrule_lemma = standard (Goal.prove thy6 [] []
   6.166        (Logic.mk_implies
   6.167          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
   6.168 -         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls)))) (fn prems =>
   6.169 -           [cut_facts_tac prems 1, REPEAT (etac conjE 1),
   6.170 +         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
   6.171 +           [REPEAT (etac conjE 1),
   6.172              REPEAT (EVERY
   6.173                [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
   6.174 -               etac mp 1, resolve_tac iso_elem_thms 1])]);
   6.175 +               etac mp 1, resolve_tac iso_elem_thms 1])]));
   6.176  
   6.177      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   6.178      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   6.179        map (Free o apfst fst o dest_Var) Ps;
   6.180      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
   6.181  
   6.182 -    val dt_induct = OldGoals.prove_goalw_cterm [] (cert
   6.183 -      (DatatypeProp.make_ind descr sorts)) (fn prems =>
   6.184 +    val dt_induct_prop = DatatypeProp.make_ind descr sorts;
   6.185 +    val dt_induct = standard (Goal.prove thy6 []
   6.186 +      (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   6.187 +      (fn prems => EVERY
   6.188          [rtac indrule_lemma' 1,
   6.189           (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   6.190           EVERY (map (fn (prem, r) => (EVERY
   6.191             [REPEAT (eresolve_tac Abs_inverse_thms 1),
   6.192              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   6.193              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   6.194 -                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   6.195 +                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]));
   6.196  
   6.197      val (thy7, [dt_induct']) = thy6 |>
   6.198        Theory.add_path big_name |>
     7.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Oct 22 01:22:10 2005 +0200
     7.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 25 18:18:49 2005 +0200
     7.3 @@ -248,7 +248,7 @@
     7.4    | ap_split _ _ _ _ u =  u;
     7.5  
     7.6  fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
     7.7 -      if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
     7.8 +      if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms,
     7.9          mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms)))
    7.10        else t
    7.11    | mk_tuple _ _ _ (t::_) = t;
    7.12 @@ -286,7 +286,7 @@
    7.13  
    7.14  val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
    7.15  
    7.16 -val all_not_allowed = 
    7.17 +val all_not_allowed =
    7.18      "Introduction rule must not have a leading \"!!\" quantifier";
    7.19  
    7.20  fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
    7.21 @@ -472,10 +472,11 @@
    7.22  
    7.23  fun prove_mono setT fp_fun monos thy =
    7.24   (message "  Proving monotonicity ...";
    7.25 -  OldGoals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
    7.26 -    (Thm.cterm_of thy (HOLogic.mk_Trueprop
    7.27 -      (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    7.28 -    (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
    7.29 +  standard (Goal.prove thy [] []   (*NO quick_and_dirty here!*)
    7.30 +    (HOLogic.mk_Trueprop
    7.31 +      (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun))
    7.32 +    (fn _ => EVERY [rtac monoI 1,
    7.33 +      REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)])));
    7.34  
    7.35  
    7.36  (* prove introduction rules *)
    7.37 @@ -491,20 +492,18 @@
    7.38        | select_disj _ 1 = [rtac disjI1]
    7.39        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    7.40  
    7.41 -    val intrs = map (fn (i, intr) => OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    7.42 -      (Thm.cterm_of thy intr) (fn prems =>
    7.43 -       [(*insert prems and underlying sets*)
    7.44 -       cut_facts_tac prems 1,
    7.45 -       stac unfold 1,
    7.46 -       REPEAT (resolve_tac [vimageI2, CollectI] 1),
    7.47 -       (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
    7.48 -       EVERY1 (select_disj (length intr_ts) i),
    7.49 -       (*Not ares_tac, since refl must be tried before any equality assumptions;
    7.50 -         backtracking may occur if the premises have extra variables!*)
    7.51 -       DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
    7.52 -       (*Now solve the equations like Inl 0 = Inl ?b2*)
    7.53 -       REPEAT (rtac refl 1)])
    7.54 -      |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
    7.55 +    val intrs = (1 upto (length intr_ts) ~~ intr_ts) |> map (fn (i, intr) =>
    7.56 +      rulify (standard (SkipProof.prove thy [] [] intr (fn _ => EVERY
    7.57 +       [rewrite_goals_tac rec_sets_defs,
    7.58 +        stac unfold 1,
    7.59 +        REPEAT (resolve_tac [vimageI2, CollectI] 1),
    7.60 +        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
    7.61 +        EVERY1 (select_disj (length intr_ts) i),
    7.62 +        (*Not ares_tac, since refl must be tried before any equality assumptions;
    7.63 +          backtracking may occur if the premises have extra variables!*)
    7.64 +        DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
    7.65 +        (*Now solve the equations like Inl 0 = Inl ?b2*)
    7.66 +        REPEAT (rtac refl 1)]))))
    7.67  
    7.68    in (intrs, unfold) end;
    7.69  
    7.70 @@ -519,13 +518,16 @@
    7.71      val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
    7.72    in
    7.73      mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
    7.74 -      OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    7.75 -        (Thm.cterm_of thy t) (fn prems =>
    7.76 +      SkipProof.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    7.77 +        (fn prems => EVERY
    7.78            [cut_facts_tac [hd prems] 1,
    7.79 +           rewrite_goals_tac rec_sets_defs,
    7.80             dtac (unfold RS subst) 1,
    7.81             REPEAT (FIRSTGOAL (eresolve_tac rules1)),
    7.82             REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    7.83 -           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
    7.84 +           EVERY (map (fn prem =>
    7.85 +             DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_sets_defs prem, conjI] 1)) (tl prems))])
    7.86 +        |> standard
    7.87          |> rulify
    7.88          |> RuleCases.name cases)
    7.89    end;
    7.90 @@ -624,9 +626,9 @@
    7.91        mk_indrule cs cTs params intr_ts;
    7.92  
    7.93      val dummy = if !trace then
    7.94 -		(writeln "ind_prems = ";
    7.95 -		 List.app (writeln o Sign.string_of_term thy) ind_prems)
    7.96 -	    else ();
    7.97 +                (writeln "ind_prems = ";
    7.98 +                 List.app (writeln o Sign.string_of_term thy) ind_prems)
    7.99 +            else ();
   7.100  
   7.101      (* make predicate for instantiation of abstract induction rule *)
   7.102  
   7.103 @@ -648,22 +650,24 @@
   7.104      (* simplification rules for vimage and Collect *)
   7.105  
   7.106      val vimage_simps = if length cs < 2 then [] else
   7.107 -      map (fn c => OldGoals.quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
   7.108 +      map (fn c => standard (SkipProof.prove thy [] []
   7.109          (HOLogic.mk_Trueprop (HOLogic.mk_eq
   7.110            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   7.111             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   7.112 -             List.nth (preds, find_index_eq c cs)))))
   7.113 -        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   7.114 +             List.nth (preds, find_index_eq c cs))))
   7.115 +        (fn _ => EVERY
   7.116 +          [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1]))) cs;
   7.117  
   7.118      val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
   7.119  
   7.120      val dummy = if !trace then
   7.121 -		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
   7.122 -	    else ();
   7.123 +                (writeln "raw_fp_induct = "; print_thm raw_fp_induct)
   7.124 +            else ();
   7.125  
   7.126 -    val induct = OldGoals.quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
   7.127 -      (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   7.128 -        [rtac (impI RS allI) 1,
   7.129 +    val induct = standard (SkipProof.prove thy [] ind_prems ind_concl
   7.130 +      (fn prems => EVERY
   7.131 +        [rewrite_goals_tac [inductive_conj_def],
   7.132 +         rtac (impI RS allI) 1,
   7.133           DETERM (etac raw_fp_induct 1),
   7.134           rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   7.135           fold_goals_tac rec_sets_defs,
   7.136 @@ -674,16 +678,16 @@
   7.137           REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
   7.138           ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
   7.139           EVERY (map (fn prem =>
   7.140 -   	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   7.141 +           DEPTH_SOLVE_1 (ares_tac [rewrite_rule [inductive_conj_def] prem, conjI, refl] 1)) prems)]));
   7.142  
   7.143 -    val lemma = OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
   7.144 -      (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   7.145 -        [cut_facts_tac prems 1,
   7.146 +    val lemma = standard (SkipProof.prove thy [] []
   7.147 +      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
   7.148 +        [rewrite_goals_tac rec_sets_defs,
   7.149           REPEAT (EVERY
   7.150             [REPEAT (resolve_tac [conjI, impI] 1),
   7.151              TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   7.152              rewrite_goals_tac sum_case_rewrites,
   7.153 -            atac 1])])
   7.154 +            atac 1])]))
   7.155  
   7.156    in standard (split_rule factors (induct RS lemma)) end;
   7.157  
     8.1 --- a/src/HOL/Tools/primrec_package.ML	Sat Oct 22 01:22:10 2005 +0200
     8.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Oct 25 18:18:49 2005 +0200
     8.3 @@ -254,8 +254,8 @@
     8.4      val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
     8.5      val _ = message ("Proving equations for primrec function(s) " ^
     8.6        commas_quote (map fst nameTs1) ^ " ...");
     8.7 -    val simps = map (fn (_, t) => OldGoals.prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
     8.8 -        (fn _ => [rtac refl 1])) eqns;
     8.9 +    val simps = map (fn (_, t) => standard (Goal.prove thy' [] [] t
    8.10 +        (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
    8.11      val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
    8.12      val thy''' = thy''
    8.13        |> (#1 o PureThy.add_thmss [(("simps", simps'),
     9.1 --- a/src/HOL/arith_data.ML	Sat Oct 22 01:22:10 2005 +0200
     9.2 +++ b/src/HOL/arith_data.ML	Tue Oct 25 18:18:49 2005 +0200
     9.3 @@ -49,13 +49,9 @@
     9.4  
     9.5  (* prove conversions *)
     9.6  
     9.7 -val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     9.8 -
     9.9 -fun prove_conv expand_tac norm_tac sg ss tu =
    9.10 -  mk_meta_eq (OldGoals.prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
    9.11 -    (K [expand_tac, norm_tac ss]))
    9.12 -  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    9.13 -    (string_of_cterm (cterm_of sg (mk_eqv tu))));
    9.14 +fun prove_conv expand_tac norm_tac sg ss tu =  (* FIXME avoid standard *)
    9.15 +  mk_meta_eq (standard (Goal.prove sg [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    9.16 +    (K [expand_tac, norm_tac ss])));
    9.17  
    9.18  val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
    9.19    (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
    10.1 --- a/src/HOL/simpdata.ML	Sat Oct 22 01:22:10 2005 +0200
    10.2 +++ b/src/HOL/simpdata.ML	Tue Oct 25 18:18:49 2005 +0200
    10.3 @@ -253,14 +253,15 @@
    10.4          val aT = TFree ("'a", HOLogic.typeS);
    10.5          val x = Free ("x", aT);
    10.6          val y = Free ("y", aT)
    10.7 -      in OldGoals.prove_goalw_cterm [simp_implies_def]
    10.8 -        (cterm_of sign (Logic.mk_implies
    10.9 -          (mk_simp_implies (Logic.mk_equals (x, y)),
   10.10 -           mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))))
   10.11 -        (fn hyps => [REPEAT (ares_tac (meta_eq_to_obj_eq :: hyps) 1)])
   10.12 +      in standard (Goal.prove (Thm.theory_of_thm st) []
   10.13 +        [mk_simp_implies (Logic.mk_equals (x, y))]
   10.14 +        (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
   10.15 +        (fn prems => EVERY
   10.16 +         [rewrite_goals_tac [simp_implies_def],
   10.17 +          REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]))
   10.18        end
   10.19    end;
   10.20 -  
   10.21 +
   10.22  (*Congruence rules for = (instead of ==)*)
   10.23  fun mk_meta_cong rl = zero_var_indexes
   10.24    (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
    11.1 --- a/src/HOLCF/domain/theorems.ML	Sat Oct 22 01:22:10 2005 +0200
    11.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Oct 25 18:18:49 2005 +0200
    11.3 @@ -22,9 +22,12 @@
    11.4  fun inferT sg pre_tm =
    11.5    #1 (Sign.infer_types (Sign.pp sg) sg (K NONE) (K NONE) [] true ([pre_tm],propT));
    11.6  
    11.7 -fun pg'' thy defs t = let val sg = sign_of thy;
    11.8 -                          val ct = Thm.cterm_of sg (inferT sg t);
    11.9 -                      in OldGoals.prove_goalw_cterm defs ct end;
   11.10 +fun pg'' thy defs t tacs =
   11.11 +  let val t' = inferT thy t in
   11.12 +    standard (Goal.prove thy [] (Logic.strip_imp_prems t') (Logic.strip_imp_concl t')
   11.13 +      (fn prems => rewrite_goals_tac defs THEN EVERY (tacs (map (rewrite_rule defs) prems))))
   11.14 +  end;
   11.15 +
   11.16  fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf 
   11.17                                  | prems=> (cut_facts_tac prems 1)::tacsf);
   11.18  
    12.1 --- a/src/HOLCF/fixrec_package.ML	Sat Oct 22 01:22:10 2005 +0200
    12.2 +++ b/src/HOLCF/fixrec_package.ML	Tue Oct 25 18:18:49 2005 +0200
    12.3 @@ -105,11 +105,10 @@
    12.4        PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
    12.5      val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;
    12.6      
    12.7 -    fun mk_cterm t = cterm_of thy' (infer thy' t);
    12.8 -    val ctuple_unfold_ct = mk_cterm (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
    12.9 -    val ctuple_unfold_thm = OldGoals.prove_goalw_cterm [] ctuple_unfold_ct
   12.10 -          (fn _ => [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
   12.11 -                    simp_tac (simpset_of thy') 1]);
   12.12 +    val ctuple_unfold = infer thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
   12.13 +    val ctuple_unfold_thm = standard (Goal.prove thy' [] [] ctuple_unfold
   12.14 +          (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
   12.15 +                    simp_tac (simpset_of thy') 1]));
   12.16      val ctuple_induct_thm =
   12.17            (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind);
   12.18      
   12.19 @@ -216,9 +215,8 @@
   12.20  (* proves a block of pattern matching equations as theorems, using unfold *)
   12.21  fun make_simps thy (unfold_thm, eqns) =
   12.22    let
   12.23 -    fun tacsf prems =
   12.24 -      [rtac (unfold_thm RS ssubst_lhs) 1, simp_tac (simpset_of thy addsimps prems) 1];
   12.25 -    fun prove_term t = OldGoals.prove_goalw_cterm [] (cterm_of thy t) tacsf;
   12.26 +    val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1];
   12.27 +    fun prove_term t = standard (Goal.prove thy [] [] t (K (EVERY tacs)));
   12.28      fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
   12.29    in
   12.30      map prove_eqn eqns
   12.31 @@ -275,8 +273,8 @@
   12.32      val cname = case chead_of t of Const(c,_) => c | _ =>
   12.33                fixrec_err "function is not declared as constant in theory";
   12.34      val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
   12.35 -    val simp = OldGoals.prove_goalw_cterm [] (cterm_of thy eq)
   12.36 -          (fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   12.37 +    val simp = standard (Goal.prove thy [] [] eq
   12.38 +          (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]));
   12.39    in simp end;
   12.40  
   12.41  fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
    13.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Oct 22 01:22:10 2005 +0200
    13.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Oct 25 18:18:49 2005 +0200
    13.3 @@ -270,19 +270,14 @@
    13.4    val case_trans = hd con_defs RS Ind_Syntax.def_trans
    13.5    and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
    13.6  
    13.7 -  (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
    13.8 -  fun case_tacsf con_def _ =
    13.9 -    [rewtac con_def,
   13.10 -     rtac case_trans 1,
   13.11 -     REPEAT (resolve_tac [refl, split_trans,
   13.12 -                          Su.case_inl RS trans,
   13.13 -                          Su.case_inr RS trans] 1)];
   13.14 -
   13.15 -  fun prove_case_eqn (arg,con_def) =
   13.16 -      OldGoals.prove_goalw_cterm []
   13.17 -        (Ind_Syntax.traceIt "next case equation = "
   13.18 -           (cterm_of (sign_of thy1) (mk_case_eqn arg)))
   13.19 -        (case_tacsf con_def);
   13.20 +  fun prove_case_eqn (arg, con_def) =
   13.21 +    standard (Goal.prove thy1 [] []
   13.22 +      (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
   13.23 +      (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
   13.24 +      (fn _ => EVERY
   13.25 +        [rewtac con_def,
   13.26 +         rtac case_trans 1,
   13.27 +         REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]));
   13.28  
   13.29    val free_iffs = map standard (con_defs RL [Ind_Syntax.def_swap_iff]);
   13.30  
   13.31 @@ -317,17 +312,14 @@
   13.32  
   13.33          val recursor_trans = recursor_def RS def_Vrecursor RS trans;
   13.34  
   13.35 -        (*Proves a single recursor equation.*)
   13.36 -        fun recursor_tacsf _ =
   13.37 -          [rtac recursor_trans 1,
   13.38 -           simp_tac (rank_ss addsimps case_eqns) 1,
   13.39 -           IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];
   13.40 -
   13.41          fun prove_recursor_eqn arg =
   13.42 -            OldGoals.prove_goalw_cterm []
   13.43 -              (Ind_Syntax.traceIt "next recursor equation = "
   13.44 -                (cterm_of (sign_of thy1) (mk_recursor_eqn arg)))
   13.45 -              recursor_tacsf
   13.46 +          standard (Goal.prove thy1 [] []
   13.47 +            (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg))
   13.48 +            (*Proves a single recursor equation.*)
   13.49 +            (fn _ => EVERY
   13.50 +              [rtac recursor_trans 1,
   13.51 +               simp_tac (rank_ss addsimps case_eqns) 1,
   13.52 +               IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]));
   13.53        in
   13.54           map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases)
   13.55        end
   13.56 @@ -342,10 +334,12 @@
   13.57    (*Typical theorems have the form ~con1=con2, con1=con2==>False,
   13.58      con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
   13.59    fun mk_free s =
   13.60 -      OldGoals.prove_goalw (theory_of_thm elim)   (*Don't use thy1: it will be stale*)
   13.61 -                  con_defs s
   13.62 -        (fn prems => [cut_facts_tac prems 1,
   13.63 -                      fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]);
   13.64 +    let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*)
   13.65 +      standard (Goal.prove thy [] [] (Sign.read_prop thy s)
   13.66 +        (fn _ => EVERY
   13.67 +         [rewrite_goals_tac con_defs,
   13.68 +          fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]))
   13.69 +    end;
   13.70  
   13.71    val simps = case_eqns @ recursor_eqns;
   13.72  
    14.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Oct 22 01:22:10 2005 +0200
    14.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Oct 25 18:18:49 2005 +0200
    14.3 @@ -192,12 +192,10 @@
    14.4    val dummy = writeln "  Proving monotonicity...";
    14.5  
    14.6    val bnd_mono =
    14.7 -      OldGoals.prove_goalw_cterm []
    14.8 -        (cterm_of sign1
    14.9 -                  (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
   14.10 -        (fn _ =>
   14.11 -         [rtac (Collect_subset RS bnd_monoI) 1,
   14.12 -          REPEAT (ares_tac (basic_monos @ monos) 1)]);
   14.13 +    standard (Goal.prove sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
   14.14 +      (fn _ => EVERY
   14.15 +        [rtac (Collect_subset RS bnd_monoI) 1,
   14.16 +         REPEAT (ares_tac (basic_monos @ monos) 1)]));
   14.17  
   14.18    val dom_subset = standard (big_rec_def RS Fp.subs);
   14.19  
   14.20 @@ -221,10 +219,8 @@
   14.21  
   14.22    (*Type-checking is hardest aspect of proof;
   14.23      disjIn selects the correct disjunct after unfolding*)
   14.24 -  fun intro_tacsf disjIn prems =
   14.25 -    [(*insert prems and underlying sets*)
   14.26 -     cut_facts_tac prems 1,
   14.27 -     DETERM (stac unfold 1),
   14.28 +  fun intro_tacsf disjIn =
   14.29 +    [DETERM (stac unfold 1),
   14.30       REPEAT (resolve_tac [Part_eqI,CollectI] 1),
   14.31       (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
   14.32       rtac disjIn 2,
   14.33 @@ -251,12 +247,12 @@
   14.34            and g rl = rl RS disjI2
   14.35        in  accesses_bal(f, g, asm_rl)  end;
   14.36  
   14.37 -  fun prove_intr (ct, tacsf) = OldGoals.prove_goalw_cterm part_rec_defs ct tacsf;
   14.38 -
   14.39 -  val intrs = ListPair.map prove_intr
   14.40 -                (map (cterm_of sign1) intr_tms,
   14.41 -                 map intro_tacsf (mk_disj_rls(length intr_tms)))
   14.42 -               handle MetaSimplifier.SIMPLIFIER (msg,thm) => (print_thm thm; error msg);
   14.43 +  val intrs =
   14.44 +    (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
   14.45 +    |> ListPair.map (fn (t, tacs) =>
   14.46 +      standard (Goal.prove sign1 [] [] t
   14.47 +        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs))))
   14.48 +    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg);
   14.49  
   14.50    (********)
   14.51    val dummy = writeln "  Proving the elimination rule...";
   14.52 @@ -345,23 +341,21 @@
   14.53                                     ORELSE' etac FalseE));
   14.54  
   14.55       val quant_induct =
   14.56 -         OldGoals.prove_goalw_cterm part_rec_defs
   14.57 -           (cterm_of sign1
   14.58 -            (Logic.list_implies
   14.59 -             (ind_prems,
   14.60 -              FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred)))))
   14.61 -           (fn prems =>
   14.62 -            [rtac (impI RS allI) 1,
   14.63 -             DETERM (etac raw_induct 1),
   14.64 -             (*Push Part inside Collect*)
   14.65 -             full_simp_tac (min_ss addsimps [Part_Collect]) 1,
   14.66 -             (*This CollectE and disjE separates out the introduction rules*)
   14.67 -             REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
   14.68 -             (*Now break down the individual cases.  No disjE here in case
   14.69 -               some premise involves disjunction.*)
   14.70 -             REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE]
   14.71 -	                        ORELSE' bound_hyp_subst_tac)),
   14.72 -             ind_tac (rev prems) (length prems) ]);
   14.73 +       standard (Goal.prove sign1 [] ind_prems
   14.74 +         (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
   14.75 +         (fn prems => EVERY
   14.76 +           [rewrite_goals_tac part_rec_defs,
   14.77 +            rtac (impI RS allI) 1,
   14.78 +            DETERM (etac raw_induct 1),
   14.79 +            (*Push Part inside Collect*)
   14.80 +            full_simp_tac (min_ss addsimps [Part_Collect]) 1,
   14.81 +            (*This CollectE and disjE separates out the introduction rules*)
   14.82 +            REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
   14.83 +            (*Now break down the individual cases.  No disjE here in case
   14.84 +              some premise involves disjunction.*)
   14.85 +            REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE]
   14.86 +                               ORELSE' bound_hyp_subst_tac)),
   14.87 +            ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]));
   14.88  
   14.89       val dummy = if !Ind_Syntax.trace then
   14.90                   (writeln "quant_induct = "; print_thm quant_induct)
   14.91 @@ -431,15 +425,12 @@
   14.92       val lemma = (*makes the link between the two induction rules*)
   14.93         if need_mutual then
   14.94            (writeln "  Proving the mutual induction rule...";
   14.95 -           OldGoals.prove_goalw_cterm part_rec_defs
   14.96 -                 (cterm_of sign1 (Logic.mk_implies (induct_concl,
   14.97 -                                                   mutual_induct_concl)))
   14.98 -                 (fn prems =>
   14.99 -                  [cut_facts_tac prems 1,
  14.100 -                   REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
  14.101 -                           lemma_tac 1)]))
  14.102 -       else (writeln "  [ No mutual induction rule needed ]";
  14.103 -             TrueI);
  14.104 +           standard (Goal.prove sign1 [] []
  14.105 +             (Logic.mk_implies (induct_concl, mutual_induct_concl))
  14.106 +             (fn _ => EVERY
  14.107 +               [rewrite_goals_tac part_rec_defs,
  14.108 +                REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)])))
  14.109 +       else (writeln "  [ No mutual induction rule needed ]"; TrueI);
  14.110  
  14.111       val dummy = if !Ind_Syntax.trace then
  14.112                   (writeln "lemma = "; print_thm lemma)
  14.113 @@ -493,14 +484,11 @@
  14.114  
  14.115       val mutual_induct_fsplit =
  14.116         if need_mutual then
  14.117 -         OldGoals.prove_goalw_cterm []
  14.118 -               (cterm_of sign1
  14.119 -                (Logic.list_implies
  14.120 -                   (map (induct_prem (rec_tms~~preds)) intr_tms,
  14.121 -                    mutual_induct_concl)))
  14.122 -               (fn prems =>
  14.123 -                [rtac (quant_induct RS lemma) 1,
  14.124 -                 mutual_ind_tac (rev prems) (length prems)])
  14.125 +         standard (Goal.prove sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
  14.126 +           mutual_induct_concl
  14.127 +           (fn prems => EVERY
  14.128 +             [rtac (quant_induct RS lemma) 1,
  14.129 +              mutual_ind_tac (rev prems) (length prems)]))
  14.130         else TrueI;
  14.131  
  14.132       (** Uncurrying the predicate in the ordinary induction rule **)
    15.1 --- a/src/ZF/Tools/primrec_package.ML	Sat Oct 22 01:22:10 2005 +0200
    15.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Oct 25 18:18:49 2005 +0200
    15.3 @@ -181,10 +181,10 @@
    15.4  
    15.5      val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
    15.6      val eqn_thms =
    15.7 -      (message ("Proving equations for primrec function " ^ fname);
    15.8 -      map (fn t => OldGoals.prove_goalw_cterm rewrites
    15.9 -        (Ind_Syntax.traceIt "next primrec equation = " (cterm_of (sign_of thy1) t))
   15.10 -        (fn _ => [rtac refl 1])) eqn_terms);
   15.11 +     (message ("Proving equations for primrec function " ^ fname);
   15.12 +      eqn_terms |> map (fn t =>
   15.13 +        standard (Goal.prove thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
   15.14 +          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))));
   15.15  
   15.16      val (thy2, eqn_thms') = thy1 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
   15.17      val thy3 = thy2