src/HOL/Tools/datatype_abs_proofs.ML
changeset 28839 32d498cf7595
parent 28524 644b62cf678f
child 28965 1de908189869
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -214,7 +214,7 @@
           (map cert insts)) induct;
         val (tac, _) = Library.foldl mk_unique_tac
           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
-              THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
+              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs),
             descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
 
       in split_conj_thm (SkipProof.prove_global thy1 [] []