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