src/HOL/Tools/datatype_abs_proofs.ML
changeset 28839 32d498cf7595
parent 28524 644b62cf678f
child 28965 1de908189869
equal deleted inserted replaced
28838:d5db6dfcb34a 28839:32d498cf7595
   212           ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   212           ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   213         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
   213         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
   214           (map cert insts)) induct;
   214           (map cert insts)) induct;
   215         val (tac, _) = Library.foldl mk_unique_tac
   215         val (tac, _) = Library.foldl mk_unique_tac
   216           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
   216           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
   217               THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
   217               THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs),
   218             descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
   218             descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
   219 
   219 
   220       in split_conj_thm (SkipProof.prove_global thy1 [] []
   220       in split_conj_thm (SkipProof.prove_global thy1 [] []
   221         (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
   221         (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
   222       end;
   222       end;