diff -r 329bc52b4b86 -r 750c5a47400b src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/Provers/hypsubst.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -131,7 +131,7 @@
       let
         val (k, _) = eq_var bnd true Bi
         val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
-          setmksimps (K (mk_eqs bnd))
+          |> Simplifier.set_mksimps (K (mk_eqs bnd))
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
         etac thin_rl i, rotate_tac (~k) i]
       end handle THM _ => no_tac | EQ_VAR => no_tac) i st