src/HOL/Tools/inductive_package.ML
changeset 13197 0567f4fd1415
parent 12922 ed70a600f0ea
child 13626 282fbabec862
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri May 31 18:48:31 2002 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri May 31 18:49:31 2002 +0200
     1.3 @@ -294,7 +294,7 @@
     1.4  val all_not_allowed = 
     1.5      "Introduction rule must not have a leading \"!!\" quantifier";
     1.6  
     1.7 -fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize;
     1.8 +fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize [];
     1.9  
    1.10  in
    1.11