src/HOL/Tools/inductive.ML
changeset 41228 e1fce873b814
parent 41075 4bed56dc95fb
child 41792 ff3cb0c418b7
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Dec 17 16:25:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Dec 17 17:08:56 2010 +0100
     1.3 @@ -282,7 +282,7 @@
     1.4  
     1.5  val bad_app = "Inductive predicate must be applied to parameter(s) ";
     1.6  
     1.7 -fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
     1.8 +fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize [];
     1.9  
    1.10  in
    1.11