src/HOL/Tools/inductive_package.ML
changeset 11770 b6bb7a853dd2
parent 11755 d12864826f4c
child 11781 a08b62908caa
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Oct 14 22:07:01 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Oct 14 22:08:29 2001 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4  val all_not_allowed = 
     1.5      "Introduction rule must not have a leading \"!!\" quantifier";
     1.6  
     1.7 -val atomize_cterm = full_rewrite_cterm inductive_atomize;
     1.8 +val atomize_cterm = rewrite_cterm true inductive_atomize;
     1.9  
    1.10  in
    1.11