src/HOL/Nominal/nominal_atoms.ML
changeset 59940 087d81f5213e
parent 59936 b8ffc3dc9e24
child 60003 ba8fa0c38d66
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 22:11:01 2015 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 06 23:14:05 2015 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  val finite_emptyI = @{thm "finite.emptyI"};
     1.5  val Collect_const = @{thm "Collect_const"};
     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  
    1.10  
    1.11  (* theory data *)