diff -r 11e7ee2ca77f -r e1fce873b814 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Dec 17 16:25:21 2010 +0100
+++ b/src/Pure/axclass.ML	Fri Dec 17 17:08:56 2010 +0100
@@ -322,11 +322,11 @@
 
 fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
 
-fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
-fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
+fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy);
+fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy));
 
-fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
-fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
+fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
+fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
 
 fun lookup_inst_param consts params (c, T) =
   (case get_inst_tyco consts (c, T) of