--- a/Separation_Algebra/sep_tactics.ML	Fri Sep 12 00:47:15 2014 +0800
+++ b/Separation_Algebra/sep_tactics.ML	Sat Sep 13 10:07:14 2014 +0800
@@ -121,7 +121,7 @@
 
   (* simp add: sep_conj_ac *)
   val sep_conj_ac_tac = Simplifier.asm_full_simp_tac
-                          (put_simpset HOL_basic_ss ctxt addsimps SepConj.sep_conj_ac);
+                          (HOL_basic_ss addsimps SepConj.sep_conj_ac);
 
 in
   (* XXX: normally you'd want to keep track of what variables we want to make