src/HOL/Tools/legacy_transfer.ML

--- a/src/HOL/Tools/legacy_transfer.ML	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Tools/legacy_transfer.ML	Thu Apr 18 17:07:01 2013 +0200
@@ -130,7 +130,7 @@
     val (hyps, ctxt5) = ctxt4
       |> Assumption.add_assumes (map transform c_vars');
     val simpset =
-      Simplifier.context ctxt5 HOL_ss addsimps (inj @ embed @ return)
+      put_simpset HOL_ss ctxt5 addsimps (inj @ embed @ return)
       |> fold Simplifier.add_cong cong;
     val thm' = thm
       |> Drule.cterm_instantiate (c_vars ~~ c_exprs')