src/Pure/axclass.ML
changeset 41228 e1fce873b814
parent 39557 fe5722fce758
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/axclass.ML	Fri Dec 17 16:25:21 2010 +0100
     1.2 +++ b/src/Pure/axclass.ML	Fri Dec 17 17:08:56 2010 +0100
     1.3 @@ -322,11 +322,11 @@
     1.4  
     1.5  fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
     1.6  
     1.7 -fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
     1.8 -fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
     1.9 +fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy);
    1.10 +fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy));
    1.11  
    1.12 -fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
    1.13 -fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    1.14 +fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
    1.15 +fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    1.16  
    1.17  fun lookup_inst_param consts params (c, T) =
    1.18    (case get_inst_tyco consts (c, T) of