diff -r 159bab53b40d -r 3d03190d2864 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Fri Mar 06 21:49:58 2009 +0100
+++ b/src/Tools/eqsubst.ML	Fri Mar 06 22:32:27 2009 +0100
@@ -128,8 +128,7 @@
 
 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
 fun prep_meta_eq ctxt =
-  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
-  in mk #> map Drule.zero_var_indexes end;
+  Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes;
 
 
   (* a type abriviation for match information *)