--- 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 *)