src/HOL/Nominal/nominal_datatype.ML
changeset 35625 9c818cab0dd0
parent 35402 115a5a95710a
child 35742 eb8d2f668bfc
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -1074,7 +1074,7 @@
     1.4        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
     1.5        (fn {prems, ...} => EVERY
     1.6          [rtac indrule_lemma' 1,
     1.7 -         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
     1.8 +         (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
     1.9           EVERY (map (fn (prem, r) => (EVERY
    1.10             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
    1.11              simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,