src/HOL/Tools/datatype_realizer.ML
changeset 58963 26bf09b95dda
parent 58659 6c9821c32dd5
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Nov 09 20:49:28 2014 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Mon Nov 10 21:49:48 2014 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4              ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
     1.5              rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
     1.6              REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
     1.7 -              REPEAT (etac allE i) THEN atac i)) 1)])
     1.8 +              REPEAT (etac allE i) THEN assume_tac ctxt i)) 1)])
     1.9        |> Drule.export_without_context;
    1.10  
    1.11      val ind_name = Thm.derivation_name induct;