# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282456885 -28800
# Node ID 0170e0dc5f9607c4557cbdaf8793dda4e47eeda3
# Parent  b97bd93fb9e20a89ea776be9a2844c4c0d4fad5d
use a smaller simpset in order to not solve refl-instances

diff -r b97bd93fb9e2 -r 0170e0dc5f96 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Aug 22 12:58:03 2010 +0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Aug 22 14:01:25 2010 +0800
@@ -678,18 +678,19 @@
    for internal usage *)
 fun lifted ctxt qtys simps rthm =
 let
+  val ss = (mk_minimal_ss ctxt) addsimps simps
+
   (* When the theorem is atomized, eta redexes are contracted,
      so we do it both in the original theorem *)
   val rthm' =
     rthm 
-    |> asm_full_simplify (HOL_basic_ss addsimps simps)
+    |> asm_full_simplify ss
     |> Drule.eta_contraction_rule 
   val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
   val goal = derive_qtrm ctxt qtys (prop_of rthm'')
 in
   Goal.prove ctxt' [] [] goal 
-    (K ((asm_full_simp_tac (HOL_basic_ss addsimps simps)
-         THEN' lift_single_tac ctxt' rthm') 1))
+    (K ((asm_full_simp_tac ss THEN' lift_single_tac ctxt' rthm') 1))
   |> singleton (ProofContext.export ctxt' ctxt)
 end