src/ZF/Tools/inductive_package.ML
changeset 32957 675c0c7e6a37
parent 32765 3032c0308019
child 33040 cffdb7b28498
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -193,9 +193,9 @@
     1.4          [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
     1.5           REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
     1.6  
     1.7 -  val dom_subset = standard (big_rec_def RS Fp.subs);
     1.8 +  val dom_subset = Drule.standard (big_rec_def RS Fp.subs);
     1.9  
    1.10 -  val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
    1.11 +  val unfold = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.Tarski);
    1.12  
    1.13    (********)
    1.14    val dummy = writeln "  Proving the introduction rules...";
    1.15 @@ -205,7 +205,7 @@
    1.16    val Part_trans =
    1.17        case rec_names of
    1.18             [_] => asm_rl
    1.19 -         | _   => standard (@{thm Part_subset} RS @{thm subset_trans});
    1.20 +         | _   => Drule.standard (@{thm Part_subset} RS @{thm subset_trans});
    1.21  
    1.22    (*To type-check recursive occurrences of the inductive sets, possibly
    1.23      enclosed in some monotonic operator M.*)
    1.24 @@ -503,7 +503,7 @@
    1.25       val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
    1.26  
    1.27       val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
    1.28 -                  |> standard
    1.29 +                  |> Drule.standard
    1.30       and mutual_induct = CP.remove_split mutual_induct_fsplit
    1.31  
    1.32       val ([induct', mutual_induct'], thy') =
    1.33 @@ -514,7 +514,7 @@
    1.34      in ((thy', induct'), mutual_induct')
    1.35      end;  (*of induction_rules*)
    1.36  
    1.37 -  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
    1.38 +  val raw_induct = Drule.standard ([big_rec_def, bnd_mono] MRS Fp.induct)
    1.39  
    1.40    val ((thy2, induct), mutual_induct) =
    1.41      if not coind then induction_rules raw_induct thy1