src/HOL/Tools/inductive_package.ML
changeset 11781 a08b62908caa
parent 11770 b6bb7a853dd2
child 11831 d2421e124fa3
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Oct 15 20:34:44 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 15 20:35:10 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 = rewrite_cterm true inductive_atomize;
     1.8 +val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize;
     1.9  
    1.10  in
    1.11