src/ZF/intr_elim.ML
changeset 2688 889a1cbd1aca
parent 2414 13df7d6c5c3b
child 3925 90f499226ab9
     1.1 --- a/src/ZF/intr_elim.ML	Fri Feb 28 15:44:32 1997 +0100
     1.2 +++ b/src/ZF/intr_elim.ML	Fri Feb 28 15:46:41 1997 +0100
     1.3 @@ -155,7 +155,8 @@
     1.4        rule_by_tactic (rewrite_goals_tac defs THEN 
     1.5                        basic_elim_tac THEN
     1.6                        fold_tac defs)
     1.7 -        (assume_read Inductive.thy s  RS  elim);
     1.8 +         (assume_read Inductive.thy s  RS  elim)
     1.9 +      |> standard;
    1.10  
    1.11    val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
    1.12    and rec_names = rec_names