src/Tools/coherent.ML

--- a/src/Tools/coherent.ML	Mon Mar 16 19:40:03 2009 +0100
+++ b/src/Tools/coherent.ML	Mon Mar 16 23:36:55 2009 +0100
@@ -51,7 +51,7 @@
 
 end;
 
-fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
+fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
 
 (* Decompose elimination rule of the form
    A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P