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