# HG changeset patch
# User wenzelm
# Date 1369067908 -7200
# Node ID 6ce832f71bdd51ac638bc4beed812e1e925afa6f
# Parent  7d8b53e80ce781a82371f77ab83272adaaeb6196
proper context;

diff -r 7d8b53e80ce7 -r 6ce832f71bdd src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Mon May 20 18:37:35 2013 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon May 20 18:38:28 2013 +0200
@@ -722,8 +722,8 @@
                       @{thm rename_guarantees_eq_rename_inv},
                       @{thm bij_imp_bij_inv}, @{thm surj_rename},
                       @{thm inv_inv_eq}]) 1,
-    asm_simp_tac  (* FIXME ctxt !!? *)
-        (@{context} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
+    asm_simp_tac
+        (ctxt addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
 *}
 
 method_setup rename_client_map = {*