src/ZF/Tools/inductive_package.ML

 
   (********)
   val dummy = writeln "  Proving monotonicity...";
 
   val bnd_mono =
-    standard (Goal.prove sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
+    Goal.prove_global sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
       (fn _ => EVERY
         [rtac (Collect_subset RS bnd_monoI) 1,
-         REPEAT (ares_tac (basic_monos @ monos) 1)]));
+         REPEAT (ares_tac (basic_monos @ monos) 1)]);
 
   val dom_subset = standard (big_rec_def RS Fp.subs);
 
   val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
 

       in  accesses_bal(f, g, asm_rl)  end;
 
   val intrs =
     (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
     |> ListPair.map (fn (t, tacs) =>
-      standard (Goal.prove sign1 [] [] t
-        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs))))
+      Goal.prove_global sign1 [] [] t
+        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
     handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg);
 
   (********)
   val dummy = writeln "  Proving the elimination rule...";
 

                       (fn prems => resolve_tac (triv_rls@prems)
                                    ORELSE' assume_tac
                                    ORELSE' etac FalseE));
 
      val quant_induct =
-       standard (Goal.prove sign1 [] ind_prems
+       Goal.prove_global sign1 [] ind_prems
          (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
          (fn prems => EVERY
            [rewrite_goals_tac part_rec_defs,
             rtac (impI RS allI) 1,
             DETERM (etac raw_induct 1),

             REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
             (*Now break down the individual cases.  No disjE here in case
               some premise involves disjunction.*)
             REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE]
                                ORELSE' bound_hyp_subst_tac)),
-            ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]));
+            ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
 
      val dummy = if !Ind_Syntax.trace then
                  (writeln "quant_induct = "; print_thm quant_induct)
              else ();
 

      val need_mutual = length rec_names > 1;
 
      val lemma = (*makes the link between the two induction rules*)
        if need_mutual then
           (writeln "  Proving the mutual induction rule...";
-           standard (Goal.prove sign1 [] []
+           Goal.prove_global sign1 [] []
              (Logic.mk_implies (induct_concl, mutual_induct_concl))
              (fn _ => EVERY
                [rewrite_goals_tac part_rec_defs,
-                REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)])))
+                REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
        else (writeln "  [ No mutual induction rule needed ]"; TrueI);
 
      val dummy = if !Ind_Syntax.trace then
                  (writeln "lemma = "; print_thm lemma)
              else ();

                ) i)
             THEN mutual_ind_tac prems (i-1);
 
      val mutual_induct_fsplit =
        if need_mutual then
-         standard (Goal.prove sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
+         Goal.prove_global sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
            mutual_induct_concl
            (fn prems => EVERY
              [rtac (quant_induct RS lemma) 1,
-              mutual_ind_tac (rev prems) (length prems)]))
+              mutual_ind_tac (rev prems) (length prems)])
        else TrueI;
 
      (** Uncurrying the predicate in the ordinary induction rule **)
 
      (*instantiate the variable to a tuple, if it is non-trivial, in order to