1.1 --- a/src/Tools/eqsubst.ML	Fri Mar 06 21:49:58 2009 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Fri Mar 06 22:32:27 2009 +0100
     1.3 @@ -128,8 +128,7 @@
     1.4  
     1.5  (* changes object "=" to meta "==" which prepares a given rewrite rule *)
     1.6  fun prep_meta_eq ctxt =
     1.7 -  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
     1.8 -  in mk #> map Drule.zero_var_indexes end;
     1.9 +  Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes;
    1.10  
    1.11  
    1.12    (* a type abriviation for match information *)