# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260145340 -3600
# Node ID 2c95d0436a2b6aa8c5cff18109e7392fe8e91f97
# Parent  5c1e6b896ff0f979ee9a8b24d2f48ba253764d4c
removed usage of HOL_basic_ss by using a slighly extended version of empty_ss

diff -r 5c1e6b896ff0 -r 2c95d0436a2b IntEx.thy
--- a/IntEx.thy	Mon Dec 07 00:13:36 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 01:22:20 2009 +0100
@@ -156,6 +156,8 @@
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 
+thm lambda_prs
+
 lemma test2: "my_plus a = my_plus a"
 apply(rule refl)
 done
diff -r 5c1e6b896ff0 -r 2c95d0436a2b IntEx2.thy
--- a/IntEx2.thy	Mon Dec 07 00:13:36 2009 +0100
+++ b/IntEx2.thy	Mon Dec 07 01:22:20 2009 +0100
@@ -389,6 +389,7 @@
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
 use "~~/src/HOL/Tools/numeral_syntax.ML"
+(*
 setup NumeralSyntax.setup
 
 abbreviation
@@ -432,3 +433,4 @@
 
 lemmas normalize_bin_simps =
   Bit0_Pls Bit1_Min
+*)
\ No newline at end of file
diff -r 5c1e6b896ff0 -r 2c95d0436a2b QuotMain.thy
--- 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),