Goal.prove_global;
authorwenzelm
Sat Jul 08 12:54:33 2006 +0200 (2006-07-08)
changeset 200469c8909fc5865
parent 20045 e66efbafbf1f
child 20047 e23a3afaaa8a
Goal.prove_global;
TFL/rules.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/typedef_package.ML
src/HOL/simpdata.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/fixrec_package.ML
src/Pure/Tools/codegen_theorems.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 Jul 08 12:54:32 2006 +0200
     1.2 +++ b/TFL/rules.ML	Sat Jul 08 12:54:33 2006 +0200
     1.3 @@ -817,9 +817,9 @@
     1.4    let
     1.5      val {thy, t, ...} = Thm.rep_cterm ptm;
     1.6      val result =
     1.7 -      if strict then Goal.prove thy [] [] t (K tac)
     1.8 -      else Goal.prove thy [] [] t (K tac)
     1.9 +      if strict then Goal.prove_global thy [] [] t (K tac)
    1.10 +      else Goal.prove_global thy [] [] t (K tac)
    1.11          handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg);
    1.12 -  in #1 (freeze_thaw (standard result)) end;
    1.13 +  in #1 (freeze_thaw result) end;
    1.14  
    1.15  end;
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 08 12:54:32 2006 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 08 12:54:33 2006 +0200
     2.3 @@ -175,7 +175,7 @@
     2.4          val proof = fn _ => auto_tac (claset(),simp_s);
     2.5  
     2.6        in 
     2.7 -        ((name, standard (Goal.prove thy5 [] [] statement proof)), []) 
     2.8 +        ((name, Goal.prove_global thy5 [] [] statement proof), []) 
     2.9        end) ak_names_types);
    2.10  
    2.11      (* declares a perm-axclass for every atom-kind               *)
    2.12 @@ -236,7 +236,7 @@
    2.13  
    2.14          val proof = fn _ => auto_tac (claset(),simp_s);
    2.15        in 
    2.16 -        ((name, standard (Goal.prove thy7 [] [] statement proof)), []) 
    2.17 +        ((name, Goal.prove_global thy7 [] [] statement proof), []) 
    2.18        end) ak_names_types);
    2.19  
    2.20       (* declares an fs-axclass for every atom-kind       *)
    2.21 @@ -281,7 +281,7 @@
    2.22  
    2.23           val proof = fn _ => auto_tac (claset(),simp_s);
    2.24         in 
    2.25 -         ((name, standard (Goal.prove thy11 [] [] statement proof)), []) 
    2.26 +         ((name, Goal.prove_global thy11 [] [] statement proof), []) 
    2.27         end) ak_names_types);
    2.28  
    2.29         (* declares for every atom-kind combination an axclass            *)
    2.30 @@ -332,7 +332,7 @@
    2.31  
    2.32               val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1];
    2.33  	   in
    2.34 -	     PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy'
    2.35 +	     PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    2.36  	   end) 
    2.37             ak_names_types thy) ak_names_types thy12b;
    2.38         
    2.39 @@ -363,7 +363,7 @@
    2.40  
    2.41                   val proof = fn _ => auto_tac (claset(),simp_s);
    2.42  	       in
    2.43 -		PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy'
    2.44 +		PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    2.45  	       end
    2.46             else 
    2.47              ([],thy')))  (* do nothing branch, if ak_name = ak_name' *) 
     3.1 --- a/src/HOL/Nominal/nominal_package.ML	Sat Jul 08 12:54:32 2006 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Jul 08 12:54:33 2006 +0200
     3.3 @@ -255,7 +255,7 @@
     3.4      val unfolded_perm_eq_thms =
     3.5        if length descr = length new_type_names then []
     3.6        else map standard (List.drop (split_conj_thm
     3.7 -        (Goal.prove thy2 [] []
     3.8 +        (Goal.prove_global thy2 [] []
     3.9            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    3.10              (map (fn (c as (s, T), x) =>
    3.11                 let val [T1, T2] = binder_types T
    3.12 @@ -275,7 +275,7 @@
    3.13      val perm_empty_thms = List.concat (map (fn a =>
    3.14        let val permT = mk_permT (Type (a, []))
    3.15        in map standard (List.take (split_conj_thm
    3.16 -        (Goal.prove thy2 [] []
    3.17 +        (Goal.prove_global thy2 [] []
    3.18            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    3.19              (map (fn ((s, T), x) => HOLogic.mk_eq
    3.20                  (Const (s, permT --> T --> T) $
    3.21 @@ -307,7 +307,7 @@
    3.22          val pt2_ax = PureThy.get_thm thy2
    3.23            (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a));
    3.24        in List.take (map standard (split_conj_thm
    3.25 -        (Goal.prove thy2 [] []
    3.26 +        (Goal.prove_global thy2 [] []
    3.27               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    3.28                  (map (fn ((s, T), x) =>
    3.29                      let val perm = Const (s, permT --> T --> T)
    3.30 @@ -343,7 +343,7 @@
    3.31          val pt3_ax = PureThy.get_thm thy2
    3.32            (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
    3.33        in List.take (map standard (split_conj_thm
    3.34 -        (Goal.prove thy2 [] [] (Logic.mk_implies
    3.35 +        (Goal.prove_global thy2 [] [] (Logic.mk_implies
    3.36               (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    3.37                  permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
    3.38                HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    3.39 @@ -393,7 +393,7 @@
    3.40                  at_inst RS (pt_inst RS pt_perm_compose) RS sym,
    3.41                  at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
    3.42              end))
    3.43 -        val thms = split_conj_thm (standard (Goal.prove thy [] []
    3.44 +        val thms = split_conj_thm (Goal.prove_global thy [] []
    3.45              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    3.46                (map (fn ((s, T), x) =>
    3.47                    let
    3.48 @@ -408,7 +408,7 @@
    3.49                    end)
    3.50                  (perm_names ~~ Ts ~~ perm_indnames))))
    3.51            (fn _ => EVERY [indtac induction perm_indnames 1,
    3.52 -             ALLGOALS (asm_full_simp_tac simps)])))
    3.53 +             ALLGOALS (asm_full_simp_tac simps)]))
    3.54        in
    3.55          foldl (fn ((s, tvs), thy) => AxClass.prove_arity
    3.56              (s, replicate (length tvs) (cp_class :: classes), [cp_class])
    3.57 @@ -517,7 +517,7 @@
    3.58        (perm_indnames ~~ descr);
    3.59  
    3.60      fun mk_perm_closed name = map (fn th => standard (th RS mp))
    3.61 -      (List.take (split_conj_thm (Goal.prove thy4 [] []
    3.62 +      (List.take (split_conj_thm (Goal.prove_global thy4 [] []
    3.63          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
    3.64             (fn (S, x) =>
    3.65                let
    3.66 @@ -766,12 +766,12 @@
    3.67        let
    3.68          val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
    3.69          val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms
    3.70 -      in standard (Goal.prove thy8 [] [] eqn (fn _ => EVERY
    3.71 +      in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
    3.72          [resolve_tac inj_thms 1,
    3.73           rewrite_goals_tac rewrites,
    3.74           rtac refl 3,
    3.75           resolve_tac rep_intrs 2,
    3.76 -         REPEAT (resolve_tac rep_thms 1)]))
    3.77 +         REPEAT (resolve_tac rep_thms 1)])
    3.78        end;
    3.79  
    3.80      val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
    3.81 @@ -785,11 +785,11 @@
    3.82          val permT = mk_permT (Type (atom, []));
    3.83          val pi = Free ("pi", permT);
    3.84        in
    3.85 -        standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
    3.86 +        Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
    3.87              (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
    3.88               Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x))))
    3.89            (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
    3.90 -            perm_closed_thms @ Rep_thms)) 1))
    3.91 +            perm_closed_thms @ Rep_thms)) 1)
    3.92        end) Rep_thms;
    3.93  
    3.94      val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
    3.95 @@ -807,8 +807,8 @@
    3.96      fun prove_distinct_thms (_, []) = []
    3.97        | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
    3.98            let
    3.99 -            val dist_thm = standard (Goal.prove thy8 [] [] t (fn _ =>
   3.100 -              simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1))
   3.101 +            val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
   3.102 +              simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
   3.103            in dist_thm::(standard (dist_thm RS not_sym))::
   3.104              (prove_distinct_thms (p, ts))
   3.105            end;
   3.106 @@ -849,7 +849,7 @@
   3.107            val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts;
   3.108            val c = Const (cname, map fastype_of l_args ---> T)
   3.109          in
   3.110 -          standard (Goal.prove thy8 [] []
   3.111 +          Goal.prove_global thy8 [] []
   3.112              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.113                (perm (list_comb (c, l_args)), list_comb (c, r_args))))
   3.114              (fn _ => EVERY
   3.115 @@ -860,7 +860,7 @@
   3.116                   (symmetric perm_fun_def :: abs_perm)) 1),
   3.117                 TRY (simp_tac (HOL_basic_ss addsimps
   3.118                   (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
   3.119 -                    perm_closed_thms)) 1)]))
   3.120 +                    perm_closed_thms)) 1)])
   3.121          end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
   3.122        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   3.123  
   3.124 @@ -898,7 +898,7 @@
   3.125            val Ts = map fastype_of args1;
   3.126            val c = Const (cname, Ts ---> T)
   3.127          in
   3.128 -          standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.129 +          Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.130                (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
   3.131                 foldr1 HOLogic.mk_conj eqs)))
   3.132              (fn _ => EVERY
   3.133 @@ -908,7 +908,7 @@
   3.134                    alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
   3.135                    perm_rep_perm_thms)) 1),
   3.136                  TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
   3.137 -                  expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)]))
   3.138 +                  expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
   3.139          end) (constrs ~~ constr_rep_thms)
   3.140        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   3.141  
   3.142 @@ -946,7 +946,7 @@
   3.143            fun fresh t =
   3.144              Const ("Nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
   3.145                Free ("a", atomT) $ t;
   3.146 -          val supp_thm = standard (Goal.prove thy8 [] []
   3.147 +          val supp_thm = Goal.prove_global thy8 [] []
   3.148                (HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.149                  (supp c,
   3.150                   if null dts then Const ("{}", HOLogic.mk_setT atomT)
   3.151 @@ -955,15 +955,15 @@
   3.152                simp_tac (HOL_basic_ss addsimps (supp_def ::
   3.153                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
   3.154                   symmetric empty_def :: Finites.emptyI :: simp_thms @
   3.155 -                 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1))
   3.156 +                 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
   3.157          in
   3.158            (supp_thm,
   3.159 -           standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.160 +           Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.161                (fresh c,
   3.162                 if null dts then HOLogic.true_const
   3.163                 else foldr1 HOLogic.mk_conj (map fresh args2))))
   3.164               (fn _ =>
   3.165 -               simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1)))
   3.166 +               simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1))
   3.167          end) atoms) constrs)
   3.168        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
   3.169  
   3.170 @@ -985,14 +985,14 @@
   3.171      val (indrule_lemma_prems, indrule_lemma_concls) =
   3.172        Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs'));
   3.173  
   3.174 -    val indrule_lemma = standard (Goal.prove thy8 [] []
   3.175 +    val indrule_lemma = Goal.prove_global thy8 [] []
   3.176        (Logic.mk_implies
   3.177          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
   3.178           HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
   3.179             [REPEAT (etac conjE 1),
   3.180              REPEAT (EVERY
   3.181                [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
   3.182 -               etac mp 1, resolve_tac Rep_thms 1])]));
   3.183 +               etac mp 1, resolve_tac Rep_thms 1])]);
   3.184  
   3.185      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   3.186      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   3.187 @@ -1003,7 +1003,7 @@
   3.188      val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
   3.189  
   3.190      val dt_induct_prop = DatatypeProp.make_ind descr' sorts';
   3.191 -    val dt_induct = standard (Goal.prove thy8 []
   3.192 +    val dt_induct = Goal.prove_global thy8 []
   3.193        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   3.194        (fn prems => EVERY
   3.195          [rtac indrule_lemma' 1,
   3.196 @@ -1012,7 +1012,7 @@
   3.197             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
   3.198              simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
   3.199              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   3.200 -                (prems ~~ constr_defs))]));
   3.201 +                (prems ~~ constr_defs))]);
   3.202  
   3.203      val case_names_induct = mk_case_names_induct descr'';
   3.204  
   3.205 @@ -1028,7 +1028,7 @@
   3.206      val finite_supp_thms = map (fn atom =>
   3.207        let val atomT = Type (atom, [])
   3.208        in map standard (List.take
   3.209 -        (split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop
   3.210 +        (split_conj_thm (Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop
   3.211             (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem
   3.212               (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
   3.213                Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT))))
   3.214 @@ -1258,7 +1258,7 @@
   3.215  
   3.216      val _ = warning "proving strong induction theorem ...";
   3.217  
   3.218 -    val induct_aux = standard (Goal.prove thy9 [] ind_prems' ind_concl'
   3.219 +    val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl'
   3.220        (fn prems => EVERY
   3.221          ([mk_subgoal 1 (K (K (K aux_ind_concl))),
   3.222            indtac dt_induct tnames 1] @
   3.223 @@ -1310,7 +1310,7 @@
   3.224                 (constrs ~~ constrs'))) (descr'' ~~ ndescr)) @
   3.225           [REPEAT (eresolve_tac [conjE, allE_Nil] 1),
   3.226            REPEAT (etac allE 1),
   3.227 -          REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)])));
   3.228 +          REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)]));
   3.229  
   3.230      val induct_aux' = Thm.instantiate ([],
   3.231        map (fn (s, T) =>
   3.232 @@ -1323,12 +1323,12 @@
   3.233            cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
   3.234          end) fresh_fs) induct_aux;
   3.235  
   3.236 -    val induct = standard (Goal.prove thy9 [] ind_prems ind_concl
   3.237 +    val induct = Goal.prove_global thy9 [] ind_prems ind_concl
   3.238        (fn prems => EVERY
   3.239           [rtac induct_aux' 1,
   3.240            REPEAT (resolve_tac induct_aux_lemmas 1),
   3.241            REPEAT ((resolve_tac prems THEN_ALL_NEW
   3.242 -            (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)]))
   3.243 +            (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
   3.244  
   3.245      val (_, thy10) = thy9 |>
   3.246        Theory.add_path big_name |>
   3.247 @@ -1430,19 +1430,19 @@
   3.248               HOLogic.mk_mem (HOLogic.mk_prod (mk_perm [] (pi, x), mk_perm [] (pi, y)), R'))
   3.249            end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
   3.250          val ths = map (fn th => standard (th RS mp)) (split_conj_thm
   3.251 -          (Goal.prove thy11 [] []
   3.252 +          (Goal.prove_global thy11 [] []
   3.253              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps)))
   3.254              (fn _ => rtac rec_induct 1 THEN REPEAT
   3.255                 (NominalPermeq.perm_simp_tac (simpset_of thy11) 1 THEN
   3.256                  (resolve_tac rec_intrs THEN_ALL_NEW
   3.257                   asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1))))
   3.258 -        val ths' = map (fn ((P, Q), th) => standard
   3.259 -          (Goal.prove thy11 [] []
   3.260 +        val ths' = map (fn ((P, Q), th) =>
   3.261 +          Goal.prove_global thy11 [] []
   3.262              (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))
   3.263              (fn _ => dtac (Thm.instantiate ([],
   3.264                   [(cterm_of thy11 (Var (("pi", 0), permT)),
   3.265                     cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
   3.266 -               NominalPermeq.perm_simp_tac HOL_ss 1))) (ps ~~ ths)
   3.267 +               NominalPermeq.perm_simp_tac HOL_ss 1)) (ps ~~ ths)
   3.268        in (ths, ths') end) dt_atomTs);
   3.269  
   3.270      (** finite support **)
   3.271 @@ -1458,7 +1458,7 @@
   3.272              (rec_fns ~~ rec_fn_Ts)
   3.273        in
   3.274          map (fn th => standard (th RS mp)) (split_conj_thm
   3.275 -          (Goal.prove thy11 [] fins
   3.276 +          (Goal.prove_global thy11 [] fins
   3.277              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   3.278                (map (fn (((T, U), R), i) =>
   3.279                   let
     4.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Jul 08 12:54:32 2006 +0200
     4.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Jul 08 12:54:33 2006 +0200
     4.3 @@ -74,12 +74,12 @@
     4.4            (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
     4.5  
     4.6        in
     4.7 -        standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
     4.8 +        Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
     4.9            (fn prems => EVERY
    4.10              [rtac induct' 1,
    4.11               REPEAT (rtac TrueI 1),
    4.12               REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    4.13 -             REPEAT (rtac TrueI 1)]))
    4.14 +             REPEAT (rtac TrueI 1)])
    4.15        end;
    4.16  
    4.17      val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
    4.18 @@ -216,8 +216,8 @@
    4.19                THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
    4.20              descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
    4.21  
    4.22 -      in split_conj_thm (standard (Goal.prove thy1 [] []
    4.23 -        (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac)))
    4.24 +      in split_conj_thm (Goal.prove_global thy1 [] []
    4.25 +        (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
    4.26        end;
    4.27  
    4.28      val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
    4.29 @@ -250,13 +250,13 @@
    4.30  
    4.31      val _ = message "Proving characteristic theorems for primrec combinators ..."
    4.32  
    4.33 -    val rec_thms = map (fn t => standard (Goal.prove thy2 [] [] t
    4.34 +    val rec_thms = map (fn t => Goal.prove_global thy2 [] [] t
    4.35        (fn _ => EVERY
    4.36          [rewrite_goals_tac reccomb_defs,
    4.37           rtac the1_equality 1,
    4.38           resolve_tac rec_unique_thms 1,
    4.39           resolve_tac rec_intrs 1,
    4.40 -         REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)])))
    4.41 +         REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
    4.42             (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
    4.43  
    4.44    in
    4.45 @@ -329,8 +329,8 @@
    4.46          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
    4.47            (Library.take (length newTs, reccomb_names)));
    4.48  
    4.49 -    val case_thms = map (map (fn t => standard (Goal.prove thy2 [] [] t
    4.50 -      (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))))
    4.51 +    val case_thms = map (map (fn t => Goal.prove_global thy2 [] [] t
    4.52 +      (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
    4.53            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    4.54  
    4.55    in
    4.56 @@ -362,8 +362,8 @@
    4.57          val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
    4.58            (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
    4.59        in
    4.60 -        (standard (Goal.prove thy [] [] t1 tacf),
    4.61 -         standard (Goal.prove thy [] [] t2 tacf))
    4.62 +        (Goal.prove_global thy [] [] t1 tacf,
    4.63 +         Goal.prove_global thy [] [] t2 tacf)
    4.64        end;
    4.65  
    4.66      val split_thm_pairs = map prove_split_thms
    4.67 @@ -432,8 +432,8 @@
    4.68  
    4.69      val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
    4.70  
    4.71 -    val size_thms = map (fn t => standard (Goal.prove thy' [] [] t
    4.72 -      (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])))
    4.73 +    val size_thms = map (fn t => Goal.prove_global thy' [] [] t
    4.74 +      (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))
    4.75          (DatatypeProp.make_size descr sorts thy')
    4.76  
    4.77    in
    4.78 @@ -447,8 +447,8 @@
    4.79  fun prove_weak_case_congs new_type_names descr sorts thy =
    4.80    let
    4.81      fun prove_weak_case_cong t =
    4.82 -       standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    4.83 -         (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1]))
    4.84 +       Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    4.85 +         (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1])
    4.86  
    4.87      val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
    4.88        new_type_names descr sorts thy)
    4.89 @@ -468,10 +468,10 @@
    4.90                hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
    4.91            | tac i n = rtac disjI2 i THEN tac i (n - 1)
    4.92        in 
    4.93 -        standard (Goal.prove thy [] [] t (fn _ =>
    4.94 +        Goal.prove_global thy [] [] t (fn _ =>
    4.95            EVERY [rtac allI 1,
    4.96             exh_tac (K exhaustion) 1,
    4.97 -           ALLGOALS (fn i => tac i (i-1))]))
    4.98 +           ALLGOALS (fn i => tac i (i-1))])
    4.99        end;
   4.100  
   4.101      val nchotomys =
   4.102 @@ -490,14 +490,14 @@
   4.103          val nchotomy'' = cterm_instantiate
   4.104            [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
   4.105        in
   4.106 -        standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   4.107 +        Goal.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   4.108            (fn prems => 
   4.109              let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
   4.110              in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
   4.111                  cut_facts_tac [nchotomy''] 1,
   4.112                  REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
   4.113                  REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
   4.114 -            end))
   4.115 +            end)
   4.116        end;
   4.117  
   4.118      val case_congs = map prove_case_cong (DatatypeProp.make_case_congs
     5.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jul 08 12:54:32 2006 +0200
     5.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jul 08 12:54:33 2006 +0200
     5.3 @@ -278,20 +278,20 @@
     5.4          val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
     5.5  
     5.6          val inj_Abs_thm = 
     5.7 -	    standard (Goal.prove sg [] []
     5.8 -	      (HOLogic.mk_Trueprop 
     5.9 -		(Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
    5.10 -		 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))
    5.11 -              (fn _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1]));
    5.12 +            Goal.prove_global sg [] []
    5.13 +              (HOLogic.mk_Trueprop 
    5.14 +                (Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
    5.15 +                 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))
    5.16 +              (fn _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1]);
    5.17  
    5.18          val setT = HOLogic.mk_setT T
    5.19  
    5.20          val inj_Rep_thm =
    5.21 -	    standard (Goal.prove sg [] []
    5.22 -	      (HOLogic.mk_Trueprop
    5.23 -		(Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
    5.24 -		 Const (Rep_name, RepT) $ Const ("UNIV", setT)))
    5.25 -              (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1]));
    5.26 +            Goal.prove_global sg [] []
    5.27 +              (HOLogic.mk_Trueprop
    5.28 +                (Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
    5.29 +                 Const (Rep_name, RepT) $ Const ("UNIV", setT)))
    5.30 +              (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1]);
    5.31  
    5.32        in (inj_Abs_thm, inj_Rep_thm) end;
    5.33  
    5.34 @@ -372,8 +372,8 @@
    5.35          (* prove characteristic equations *)
    5.36  
    5.37          val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
    5.38 -        val char_thms' = map (fn eqn => standard (Goal.prove thy' [] [] eqn
    5.39 -          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
    5.40 +        val char_thms' = map (fn eqn => Goal.prove_global thy' [] [] eqn
    5.41 +          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
    5.42  
    5.43        in (thy', char_thms' @ char_thms) end;
    5.44  
    5.45 @@ -394,12 +394,12 @@
    5.46              val Ts = map (TFree o rpair HOLogic.typeS)
    5.47                (variantlist (replicate i "'t", used));
    5.48              val f = Free ("f", Ts ---> U)
    5.49 -          in standard (Goal.prove sign [] [] (Logic.mk_implies
    5.50 +          in Goal.prove_global sign [] [] (Logic.mk_implies
    5.51              (HOLogic.mk_Trueprop (HOLogic.list_all
    5.52                 (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
    5.53               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
    5.54                 r $ (a $ app_bnds f i)), f))))
    5.55 -            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1]))
    5.56 +            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])
    5.57            end
    5.58        in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
    5.59  
    5.60 @@ -427,7 +427,7 @@
    5.61          val inj_thms' = map (fn r => r RS injD)
    5.62            (map snd newT_iso_inj_thms @ inj_thms);
    5.63  
    5.64 -        val inj_thm = standard (Goal.prove thy5 [] []
    5.65 +        val inj_thm = Goal.prove_global thy5 [] []
    5.66            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    5.67              [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    5.68               REPEAT (EVERY
    5.69 @@ -447,18 +447,18 @@
    5.70                           REPEAT (eresolve_tac (mp :: allE ::
    5.71                             map make_elim (Suml_inject :: Sumr_inject ::
    5.72                               Lim_inject :: fun_cong :: inj_thms')) 1),
    5.73 -                         atac 1]))])])])]));
    5.74 +                         atac 1]))])])])]);
    5.75  
    5.76          val inj_thms'' = map (fn r => r RS datatype_injI)
    5.77                               (split_conj_thm inj_thm);
    5.78  
    5.79          val elem_thm = 
    5.80 -	    standard (Goal.prove thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    5.81 -	      (fn _ =>
    5.82 -	       EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    5.83 -		rewrite_goals_tac rewrites,
    5.84 -		REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    5.85 -                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]));
    5.86 +            Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    5.87 +              (fn _ =>
    5.88 +               EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    5.89 +                rewrite_goals_tac rewrites,
    5.90 +                REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    5.91 +                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
    5.92  
    5.93        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
    5.94        end;
    5.95 @@ -489,7 +489,7 @@
    5.96  
    5.97      val iso_thms = if length descr = 1 then [] else
    5.98        Library.drop (length newTs, split_conj_thm
    5.99 -        (standard (Goal.prove thy5 [] [] iso_t (fn _ => EVERY
   5.100 +        (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
   5.101             [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   5.102              REPEAT (rtac TrueI 1),
   5.103              rewrite_goals_tac (mk_meta_eq choice_eq ::
   5.104 @@ -500,7 +500,7 @@
   5.105                   List.concat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
   5.106                 TRY (hyp_subst_tac 1),
   5.107                 rtac (sym RS range_eqI) 1,
   5.108 -               resolve_tac iso_char_thms 1])]))));
   5.109 +               resolve_tac iso_char_thms 1])])));
   5.110  
   5.111      val Abs_inverse_thms' =
   5.112        map #1 newT_iso_axms @
   5.113 @@ -519,12 +519,12 @@
   5.114        let
   5.115          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
   5.116          val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
   5.117 -      in standard (Goal.prove thy5 [] [] eqn (fn _ => EVERY
   5.118 +      in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
   5.119          [resolve_tac inj_thms 1,
   5.120           rewrite_goals_tac rewrites,
   5.121           rtac refl 1,
   5.122           resolve_tac rep_intrs 2,
   5.123 -         REPEAT (resolve_tac iso_elem_thms 1)]))
   5.124 +         REPEAT (resolve_tac iso_elem_thms 1)])
   5.125        end;
   5.126  
   5.127      (*--------------------------------------------------------------*)
   5.128 @@ -541,8 +541,8 @@
   5.129      fun prove_distinct_thms (_, []) = []
   5.130        | prove_distinct_thms (dist_rewrites', t::_::ts) =
   5.131            let
   5.132 -            val dist_thm = standard (Goal.prove thy5 [] [] t (fn _ =>
   5.133 -              EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]))
   5.134 +            val dist_thm = Goal.prove_global thy5 [] [] t (fn _ =>
   5.135 +              EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
   5.136            in dist_thm::(standard (dist_thm RS not_sym))::
   5.137              (prove_distinct_thms (dist_rewrites', ts))
   5.138            end;
   5.139 @@ -562,7 +562,7 @@
   5.140          ((map (fn r => r RS injD) iso_inj_thms) @
   5.141            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
   5.142             Lim_inject, Suml_inject, Sumr_inject]))
   5.143 -      in standard (Goal.prove thy5 [] [] t (fn _ => EVERY
   5.144 +      in Goal.prove_global thy5 [] [] t (fn _ => EVERY
   5.145          [rtac iffI 1,
   5.146           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   5.147           dresolve_tac rep_congs 1, dtac box_equals 1,
   5.148 @@ -570,7 +570,7 @@
   5.149           REPEAT (eresolve_tac inj_thms 1),
   5.150           REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
   5.151             REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
   5.152 -           atac 1]))]))
   5.153 +           atac 1]))])
   5.154        end;
   5.155  
   5.156      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   5.157 @@ -612,14 +612,14 @@
   5.158  
   5.159      val cert = cterm_of (Theory.sign_of thy6);
   5.160  
   5.161 -    val indrule_lemma = standard (Goal.prove thy6 [] []
   5.162 +    val indrule_lemma = Goal.prove_global thy6 [] []
   5.163        (Logic.mk_implies
   5.164          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
   5.165           HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
   5.166             [REPEAT (etac conjE 1),
   5.167              REPEAT (EVERY
   5.168                [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
   5.169 -               etac mp 1, resolve_tac iso_elem_thms 1])]));
   5.170 +               etac mp 1, resolve_tac iso_elem_thms 1])]);
   5.171  
   5.172      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   5.173      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   5.174 @@ -627,7 +627,7 @@
   5.175      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
   5.176  
   5.177      val dt_induct_prop = DatatypeProp.make_ind descr sorts;
   5.178 -    val dt_induct = standard (Goal.prove thy6 []
   5.179 +    val dt_induct = Goal.prove_global thy6 []
   5.180        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   5.181        (fn prems => EVERY
   5.182          [rtac indrule_lemma' 1,
   5.183 @@ -636,7 +636,7 @@
   5.184             [REPEAT (eresolve_tac Abs_inverse_thms 1),
   5.185              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   5.186              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   5.187 -                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]));
   5.188 +                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   5.189  
   5.190      val ([dt_induct'], thy7) =
   5.191        thy6
     6.1 --- a/src/HOL/Tools/primrec_package.ML	Sat Jul 08 12:54:32 2006 +0200
     6.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Jul 08 12:54:33 2006 +0200
     6.3 @@ -259,8 +259,8 @@
     6.4      val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
     6.5      val _ = message ("Proving equations for primrec function(s) " ^
     6.6        commas_quote (map fst nameTs1) ^ " ...");
     6.7 -    val simps = map (fn (_, t) => standard (Goal.prove thy' [] [] t
     6.8 -        (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
     6.9 +    val simps = map (fn (_, t) => Goal.prove_global thy' [] [] t
    6.10 +        (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
    6.11      val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
    6.12      val thy''' = thy''
    6.13        |> (snd o PureThy.add_thmss [(("simps", simps'),
     7.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Jul 08 12:54:32 2006 +0200
     7.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Jul 08 12:54:33 2006 +0200
     7.3 @@ -163,7 +163,7 @@
     7.4           (Abs_name, oldT --> newT, NoSyn)])
     7.5        |> add_def (Logic.mk_defpair (setC, set))
     7.6        ||>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
     7.7 -          [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
     7.8 +          [apsnd (fn cond_axm => nonempty RS cond_axm)])]
     7.9        ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
    7.10        ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps
    7.11        |-> (fn (set_def, [type_definition]) => fn thy1 =>
    7.12 @@ -243,7 +243,7 @@
    7.13      val (cset, goal, _, typedef_result) =
    7.14        prepare_typedef prep_term def name typ set opt_morphs thy;
    7.15      val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    7.16 -    val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg =>
    7.17 +    val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
    7.18        cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    7.19    in
    7.20      Context.Theory thy
     8.1 --- a/src/HOL/simpdata.ML	Sat Jul 08 12:54:32 2006 +0200
     8.2 +++ b/src/HOL/simpdata.ML	Sat Jul 08 12:54:33 2006 +0200
     8.3 @@ -264,12 +264,12 @@
     8.4          val aT = TFree ("'a", HOLogic.typeS);
     8.5          val x = Free ("x", aT);
     8.6          val y = Free ("y", aT)
     8.7 -      in standard (Goal.prove (Thm.theory_of_thm st) []
     8.8 +      in Goal.prove_global (Thm.theory_of_thm st) []
     8.9          [mk_simp_implies (Logic.mk_equals (x, y))]
    8.10          (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
    8.11          (fn prems => EVERY
    8.12           [rewrite_goals_tac [simp_implies_def],
    8.13 -          REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)]))
    8.14 +          REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
    8.15        end
    8.16    end;
    8.17  
     9.1 --- a/src/HOLCF/domain/theorems.ML	Sat Jul 08 12:54:32 2006 +0200
     9.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Jul 08 12:54:33 2006 +0200
     9.3 @@ -72,9 +72,7 @@
     9.4      fun tac prems =
     9.5        rewrite_goals_tac defs THEN
     9.6        EVERY (tacs (map (rewrite_rule defs) prems));
     9.7 -  in
     9.8 -    standard (Goal.prove thy [] asms prop tac)
     9.9 -  end;
    9.10 +  in Goal.prove_global thy [] asms prop tac end;
    9.11  
    9.12  fun pg' thy defs t tacsf =
    9.13    let
    10.1 --- a/src/HOLCF/fixrec_package.ML	Sat Jul 08 12:54:32 2006 +0200
    10.2 +++ b/src/HOLCF/fixrec_package.ML	Sat Jul 08 12:54:33 2006 +0200
    10.3 @@ -101,9 +101,9 @@
    10.4      val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;
    10.5      
    10.6      val ctuple_unfold = infer thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
    10.7 -    val ctuple_unfold_thm = standard (Goal.prove thy' [] [] ctuple_unfold
    10.8 +    val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold
    10.9            (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
   10.10 -                    simp_tac (simpset_of thy') 1]));
   10.11 +                    simp_tac (simpset_of thy') 1]);
   10.12      val ctuple_induct_thm =
   10.13            (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind);
   10.14      
   10.15 @@ -211,7 +211,7 @@
   10.16  fun make_simps thy (unfold_thm, eqns) =
   10.17    let
   10.18      val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1];
   10.19 -    fun prove_term t = standard (Goal.prove thy [] [] t (K (EVERY tacs)));
   10.20 +    fun prove_term t = Goal.prove_global thy [] [] t (K (EVERY tacs));
   10.21      fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
   10.22    in
   10.23      map prove_eqn eqns
   10.24 @@ -268,8 +268,8 @@
   10.25      val cname = case chead_of t of Const(c,_) => c | _ =>
   10.26                fixrec_err "function is not declared as constant in theory";
   10.27      val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
   10.28 -    val simp = standard (Goal.prove thy [] [] eq
   10.29 -          (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]));
   10.30 +    val simp = Goal.prove_global thy [] [] eq
   10.31 +          (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   10.32    in simp end;
   10.33  
   10.34  fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
    11.1 --- a/src/Pure/Tools/codegen_theorems.ML	Sat Jul 08 12:54:32 2006 +0200
    11.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Sat Jul 08 12:54:33 2006 +0200
    11.3 @@ -699,8 +699,8 @@
    11.4        let val cos' = rev cos 
    11.5        in (op @) (fold (mk_eq vs) (product cos' cos') ([], [])) end;
    11.6      fun mk_eq_thms tac vs_cos =
    11.7 -      map (fn t => Goal.prove thy [] []
    11.8 -        (ObjectLogic.ensure_propT thy t) (K tac) |> standard) (mk_eqs vs_cos);
    11.9 +      map (fn t => Goal.prove_global thy [] []
   11.10 +        (ObjectLogic.ensure_propT thy t) (K tac)) (mk_eqs vs_cos);
   11.11    in
   11.12      case getf_first (map (fn f => f thy) (the_datatypes_extrs thy)) dtco
   11.13       of NONE => NONE
    12.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Jul 08 12:54:32 2006 +0200
    12.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Jul 08 12:54:33 2006 +0200
    12.3 @@ -271,13 +271,13 @@
    12.4    and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
    12.5  
    12.6    fun prove_case_eqn (arg, con_def) =
    12.7 -    standard (Goal.prove thy1 [] []
    12.8 +    Goal.prove_global thy1 [] []
    12.9        (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
   12.10        (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
   12.11        (fn _ => EVERY
   12.12          [rewtac con_def,
   12.13           rtac case_trans 1,
   12.14 -         REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]));
   12.15 +         REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
   12.16  
   12.17    val free_iffs = map standard (con_defs RL [Ind_Syntax.def_swap_iff]);
   12.18  
   12.19 @@ -313,13 +313,13 @@
   12.20          val recursor_trans = recursor_def RS def_Vrecursor RS trans;
   12.21  
   12.22          fun prove_recursor_eqn arg =
   12.23 -          standard (Goal.prove thy1 [] []
   12.24 +          Goal.prove_global thy1 [] []
   12.25              (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg))
   12.26              (*Proves a single recursor equation.*)
   12.27              (fn _ => EVERY
   12.28                [rtac recursor_trans 1,
   12.29                 simp_tac (rank_ss addsimps case_eqns) 1,
   12.30 -               IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]));
   12.31 +               IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]);
   12.32        in
   12.33           map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases)
   12.34        end
   12.35 @@ -335,10 +335,10 @@
   12.36      con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
   12.37    fun mk_free s =
   12.38      let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*)
   12.39 -      standard (Goal.prove thy [] [] (Sign.read_prop thy s)
   12.40 +      Goal.prove_global thy [] [] (Sign.read_prop thy s)
   12.41          (fn _ => EVERY
   12.42           [rewrite_goals_tac con_defs,
   12.43 -          fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]))
   12.44 +          fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])
   12.45      end;
   12.46  
   12.47    val simps = case_eqns @ recursor_eqns;
    13.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Jul 08 12:54:32 2006 +0200
    13.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Jul 08 12:54:33 2006 +0200
    13.3 @@ -194,10 +194,10 @@
    13.4    val dummy = writeln "  Proving monotonicity...";
    13.5  
    13.6    val bnd_mono =
    13.7 -    standard (Goal.prove sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
    13.8 +    Goal.prove_global sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
    13.9        (fn _ => EVERY
   13.10          [rtac (Collect_subset RS bnd_monoI) 1,
   13.11 -         REPEAT (ares_tac (basic_monos @ monos) 1)]));
   13.12 +         REPEAT (ares_tac (basic_monos @ monos) 1)]);
   13.13  
   13.14    val dom_subset = standard (big_rec_def RS Fp.subs);
   13.15  
   13.16 @@ -252,8 +252,8 @@
   13.17    val intrs =
   13.18      (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
   13.19      |> ListPair.map (fn (t, tacs) =>
   13.20 -      standard (Goal.prove sign1 [] [] t
   13.21 -        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs))))
   13.22 +      Goal.prove_global sign1 [] [] t
   13.23 +        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
   13.24      handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg);
   13.25  
   13.26    (********)
   13.27 @@ -343,7 +343,7 @@
   13.28                                     ORELSE' etac FalseE));
   13.29  
   13.30       val quant_induct =
   13.31 -       standard (Goal.prove sign1 [] ind_prems
   13.32 +       Goal.prove_global sign1 [] ind_prems
   13.33           (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
   13.34           (fn prems => EVERY
   13.35             [rewrite_goals_tac part_rec_defs,
   13.36 @@ -357,7 +357,7 @@
   13.37                some premise involves disjunction.*)
   13.38              REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE]
   13.39                                 ORELSE' bound_hyp_subst_tac)),
   13.40 -            ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]));
   13.41 +            ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
   13.42  
   13.43       val dummy = if !Ind_Syntax.trace then
   13.44                   (writeln "quant_induct = "; print_thm quant_induct)
   13.45 @@ -427,11 +427,11 @@
   13.46       val lemma = (*makes the link between the two induction rules*)
   13.47         if need_mutual then
   13.48            (writeln "  Proving the mutual induction rule...";
   13.49 -           standard (Goal.prove sign1 [] []
   13.50 +           Goal.prove_global sign1 [] []
   13.51               (Logic.mk_implies (induct_concl, mutual_induct_concl))
   13.52               (fn _ => EVERY
   13.53                 [rewrite_goals_tac part_rec_defs,
   13.54 -                REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)])))
   13.55 +                REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
   13.56         else (writeln "  [ No mutual induction rule needed ]"; TrueI);
   13.57  
   13.58       val dummy = if !Ind_Syntax.trace then
   13.59 @@ -486,11 +486,11 @@
   13.60  
   13.61       val mutual_induct_fsplit =
   13.62         if need_mutual then
   13.63 -         standard (Goal.prove sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
   13.64 +         Goal.prove_global sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
   13.65             mutual_induct_concl
   13.66             (fn prems => EVERY
   13.67               [rtac (quant_induct RS lemma) 1,
   13.68 -              mutual_ind_tac (rev prems) (length prems)]))
   13.69 +              mutual_ind_tac (rev prems) (length prems)])
   13.70         else TrueI;
   13.71  
   13.72       (** Uncurrying the predicate in the ordinary induction rule **)
    14.1 --- a/src/ZF/Tools/primrec_package.ML	Sat Jul 08 12:54:32 2006 +0200
    14.2 +++ b/src/ZF/Tools/primrec_package.ML	Sat Jul 08 12:54:33 2006 +0200
    14.3 @@ -183,8 +183,8 @@
    14.4      val eqn_thms =
    14.5       (message ("Proving equations for primrec function " ^ fname);
    14.6        eqn_terms |> map (fn t =>
    14.7 -        standard (Goal.prove thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
    14.8 -          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))));
    14.9 +        Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
   14.10 +          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])));
   14.11  
   14.12      val (eqn_thms', thy2) =
   14.13        thy1