src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 35625 9c818cab0dd0
parent 35410 1ea89d2a1bd4
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -209,7 +209,7 @@
     1.4          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
     1.5            (map cert insts)) induct;
     1.6          val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
     1.7 -           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
     1.8 +           (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
     1.9                THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
    1.10  
    1.11        in split_conj_thm (Skip_Proof.prove_global thy1 [] []