# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259483887 -3600
# Node ID 7ba2c16fe0c860a63f945fbd6269b174153e70af
# Parent  586e3dc4afdb04ecb2aaba55d56bc05906d379bf
Removed unnecessary HOL_ss which proved one of the subgoals.

diff -r 586e3dc4afdb -r 7ba2c16fe0c8 FSet.thy
--- a/FSet.thy	Sun Nov 29 08:48:06 2009 +0100
+++ b/FSet.thy	Sun Nov 29 09:38:07 2009 +0100
@@ -469,6 +469,7 @@
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule FUN_QUOTIENT)
diff -r 586e3dc4afdb -r 7ba2c16fe0c8 QuotMain.thy
--- a/QuotMain.thy	Sun Nov 29 08:48:06 2009 +0100
+++ b/QuotMain.thy	Sun Nov 29 09:38:07 2009 +0100
@@ -952,7 +952,7 @@
 
     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
     (* global simplification *)
-    NDT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))])
+    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
 *}
 
 ML {*