# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259672936 -3600
# Node ID 10d75457792f4a19905fff8a60d4b06b3b5bd333
# Parent  5ca4a927d7f0f75ada66eff1faf77173f7d5d22f
Removed last HOL_ss

diff -r 5ca4a927d7f0 -r 10d75457792f QuotMain.thy
--- a/QuotMain.thy	Tue Dec 01 14:04:00 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 14:08:56 2009 +0100
@@ -735,14 +735,14 @@
 *}
 
 ML {*
-fun quotient_tac quot_thms =
-  REPEAT_ALL_NEW (FIRST' 
+fun quotient_tac ctxt quot_thms =
+  REPEAT_ALL_NEW (FIRST'
     [rtac @{thm FUN_QUOTIENT},
      resolve_tac quot_thms,
      rtac @{thm IDENTITY_QUOTIENT},
      (* For functional identity quotients, (op = ---> op =) *)
      (* TODO: think about the other way around, if we need to shorten the relation *)
-     CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])
+     CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
 *}
 
 lemma FUN_REL_I:
@@ -867,11 +867,11 @@
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
     NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
-                  THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
+                  THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
     NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
-                (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
+                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms)]))),
 
     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
@@ -909,8 +909,8 @@
 
 (* TODO: This is slow *)
 ML {*
-fun allex_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot)
+fun allex_prs_tac ctxt quot =
+  (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)
 *}
 
 (* Rewrites the term with LAMBDA_PRS thm.
@@ -946,7 +946,7 @@
     val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
     val tac =
       (compose_tac (false, lpi, 2)) THEN_ALL_NEW
-      (quotient_tac quot_thms);
+      (quotient_tac ctxt quot_thms);
     val gc = Drule.strip_imp_concl (cprop_of lpi);
     val t = Goal.prove_internal [] gc (fn _ => tac 1)
     val te = @{thm eq_reflection} OF [t]