src/Provers/hypsubst.ML

--- a/src/Provers/hypsubst.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/Provers/hypsubst.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -156,7 +156,7 @@
       let
         val (k, _) = eq_var bnd true Bi
         val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
-          setmksimps (mk_eqs bnd)
+          setmksimps (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