src/HOL/intr_elim.ML
changeset 2688 889a1cbd1aca
parent 2414 13df7d6c5c3b
child 3978 7e1cfed19d94
     1.1 --- a/src/HOL/intr_elim.ML	Fri Feb 28 15:44:32 1997 +0100
     1.2 +++ b/src/HOL/intr_elim.ML	Fri Feb 28 15:46:41 1997 +0100
     1.3 @@ -144,7 +144,8 @@
     1.4    (*String s should have the form t:Si where Si is an inductive set*)
     1.5    fun mk_cases defs s = 
     1.6        rule_by_tactic (con_elim_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, mono] MRS Fp.induct)
    1.12    and rec_names = rec_names