changeset 45133 | 2214ba5bdfff |
parent 44080 | 53d95b52954c |
child 45654 | cf10bde35973 |
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Oct 12 22:21:38 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Oct 12 22:48:23 2011 +0200 @@ -174,7 +174,7 @@ val tacs1 = [ quant_tac ctxt 1, simp_tac HOL_ss 1, - InductTacs.induct_tac ctxt [[SOME "n"]] 1, + Induct_Tacs.induct_tac ctxt [[SOME "n"]] 1, simp_tac (take_ss addsimps prems) 1, TRY (safe_tac (put_claset HOL_cs ctxt))] fun con_tac _ =