--- a/QuotMain.thy	Mon Dec 07 00:13:36 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 01:22:20 2009 +0100
@@ -170,11 +170,24 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
+section {* Bounded abstraction *}
+
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
+section {* Simset setup *}
+
+(* since HOL_basic_ss is too "big", we need to set up *)
+(* our own minimal simpset                            *)
+ML {*
+fun  mk_minimal_ss ctxt =
+  Simplifier.context ctxt empty_ss
+    setsubgoaler asm_simp_tac
+    setmksimps (mksimps [])
+*}
+
 section {* atomize *}
 
 lemma atomize_eqv[atomize]:
@@ -690,7 +703,7 @@
   val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
   val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
   val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
-  val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
+  val simp_ctxt = (mk_minimal_ss ctxt) addsimprocs [simproc1, simproc2, simproc3, simproc4] 
   (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
   val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 in
@@ -1150,8 +1163,7 @@
     val thms1 = @{thms all_prs ex_prs} @ defs
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
-    fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
-      (* FIXME: use of someting smaller than HOL_basic_ss *)
+    fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [lambda_prs_tac lthy,
             simp_tac (simps thms1),