| changeset 59940 | 087d81f5213e |
| parent 59936 | b8ffc3dc9e24 |
| child 60359 | cb8828b859a1 |
--- a/src/HOL/Nominal/nominal_inductive.ML Mon Apr 06 22:11:01 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Mon Apr 06 23:14:05 2015 +0200 @@ -14,7 +14,7 @@ structure NominalInductive : NOMINAL_INDUCTIVE = struct -val inductive_forall_def = @{thm induct_forall_def}; +val inductive_forall_def = @{thm HOL.induct_forall_def}; val inductive_atomize = @{thms induct_atomize}; val inductive_rulify = @{thms induct_rulify};