# HG changeset patch
# User wenzelm
# Date 1425682445 -3600
# Node ID cb84e420fc8e77e731c36370debf9b1e8df39d75
# Parent  f643308472ce98e64654049b45e7e20216cae0b9
clarified context;

diff -r f643308472ce -r cb84e420fc8e src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Mar 06 23:53:52 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Mar 06 23:54:05 2015 +0100
@@ -100,8 +100,8 @@
   let
     val thy = Proof_Context.theory_of ctxt
     fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
-    val ty_inst = map (SOME o Thm.global_ctyp_of thy) [domain_type (fastype_of R2)]
-    val trm_inst = map (SOME o Thm.global_cterm_of thy) [R2, R1]
+    val ty_inst = map (SOME o Thm.ctyp_of ctxt) [domain_type (fastype_of R2)]
+    val trm_inst = map (SOME o Thm.cterm_of ctxt) [R2, R1]
   in
     (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
       NONE => NONE
@@ -198,11 +198,10 @@
     (Const (@{const_name Quot_True}, _) $ x) =>
       let
         val fx = fnctn x;
-        val thy = Proof_Context.theory_of ctxt;
-        val cx = Thm.global_cterm_of thy x;
-        val cfx = Thm.global_cterm_of thy fx;
-        val cxt = Thm.global_ctyp_of thy (fastype_of x);
-        val cfxt = Thm.global_ctyp_of thy (fastype_of fx);
+        val cx = Thm.cterm_of ctxt x;
+        val cfx = Thm.cterm_of ctxt fx;
+        val cxt = Thm.ctyp_of ctxt (fastype_of x);
+        val cfxt = Thm.ctyp_of ctxt (fastype_of fx);
         val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
       in
         Conv.rewr_conv thm ctrm
@@ -236,7 +235,7 @@
    assumption is different from the corresponding type in the goal.
 *)
 val apply_rsp_tac =
-  Subgoal.FOCUS (fn {concl, asms, context,...} =>
+  Subgoal.FOCUS (fn {concl, asms, context = ctxt,...} =>
     let
       val bare_concl = HOLogic.dest_Trueprop (Thm.term_of concl)
       val qt_asm = find_qt_asm (map Thm.term_of asms)
@@ -250,13 +249,12 @@
               val ty_x = fastype_of x
               val ty_b = fastype_of qt_arg
               val ty_f = range_type (fastype_of f)
-              val thy = Proof_Context.theory_of context
-              val ty_inst = map (SOME o Thm.global_ctyp_of thy) [ty_x, ty_b, ty_f]
-              val t_inst = map (SOME o Thm.global_cterm_of thy) [R2, f, g, x, y];
+              val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_x, ty_b, ty_f]
+              val t_inst = map (SOME o Thm.cterm_of ctxt) [R2, f, g, x, y];
               val inst_thm = Drule.instantiate' ty_inst
                 ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
             in
-              (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
+              (rtac inst_thm THEN' SOLVED' (quotient_tac ctxt)) 1
             end
       | _ => no_tac
     end)
@@ -265,32 +263,27 @@
    complex we rely on instantiation to tell us if it applies
 *)
 fun equals_rsp_tac R ctxt =
-  let
-    val thy = Proof_Context.theory_of ctxt
-  in
-    case try (Thm.global_cterm_of thy) R of (* There can be loose bounds in R *)
-      SOME ctm =>
-        let
-          val ty = domain_type (fastype_of R)
-        in
-          case try (Drule.instantiate' [SOME (Thm.global_ctyp_of thy ty)]
-              [SOME (Thm.global_cterm_of thy R)]) @{thm equals_rsp} of
-            SOME thm => rtac thm THEN' quotient_tac ctxt
-          | NONE => K no_tac
-        end
-    | _ => K no_tac
-  end
+  case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *)  (* FIXME fragile *)
+    SOME ctm =>
+      let
+        val ty = domain_type (fastype_of R)
+      in
+        case try (Drule.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
+            [SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
+          SOME thm => rtac thm THEN' quotient_tac ctxt
+        | NONE => K no_tac
+      end
+  | _ => K no_tac
 
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>
     (case try bare_concl goal of
       SOME (rel $ _ $ (rep $ (abs $ _))) =>
         (let
-          val thy = Proof_Context.theory_of ctxt;
           val (ty_a, ty_b) = dest_funT (fastype_of abs);
-          val ty_inst = map (SOME o Thm.global_ctyp_of thy) [ty_a, ty_b];
+          val ty_inst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b];
         in
-          case try (map (SOME o Thm.global_cterm_of thy)) [rel, abs, rep] of
+          case try (map (SOME o Thm.cterm_of ctxt)) [rel, abs, rep] of
             SOME t_inst =>
               (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
                 SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
@@ -475,11 +468,10 @@
   (case Thm.term_of ctrm of
     (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
       let
-        val thy = Proof_Context.theory_of ctxt
         val (ty_b, ty_a) = dest_funT (fastype_of r1)
         val (ty_c, ty_d) = dest_funT (fastype_of a2)
-        val tyinst = map (SOME o Thm.global_ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
-        val tinst = [NONE, NONE, SOME (Thm.global_cterm_of thy r1), NONE, SOME (Thm.global_cterm_of thy a2)]
+        val tyinst = map (SOME o Thm.ctyp_of ctxt) [ty_a, ty_b, ty_c, ty_d]
+        val tinst = [NONE, NONE, SOME (Thm.cterm_of ctxt r1), NONE, SOME (Thm.cterm_of ctxt a2)]
         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
         val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
         val thm3 = rewrite_rule ctxt @{thms id_apply[THEN eq_reflection]} thm2
@@ -488,7 +480,7 @@
           then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
           else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
         val thm4 =
-          Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy insp, Thm.global_cterm_of thy inst)]) thm3
+          Drule.instantiate_normalize ([], [(Thm.cterm_of ctxt insp, Thm.cterm_of ctxt inst)]) thm3
       in
         Conv.rewr_conv thm4 ctrm
       end
@@ -555,9 +547,8 @@
 fun gen_frees_tac ctxt =
   SUBGOAL (fn (concl, i) =>
     let
-      val thy = Proof_Context.theory_of ctxt
       val vrs = Term.add_frees concl []
-      val cvrs = map (Thm.global_cterm_of thy o Free) vrs
+      val cvrs = map (Thm.cterm_of ctxt o Free) vrs
       val concl' = apply_under_Trueprop (all_list vrs) concl
       val goal = Logic.mk_implies (concl', concl)
       val rule = Goal.prove ctxt [] [] goal
@@ -608,7 +599,6 @@
 
 fun procedure_inst ctxt rtrm qtrm =
   let
-    val thy = Proof_Context.theory_of ctxt
     val rtrm' = HOLogic.dest_Trueprop rtrm
     val qtrm' = HOLogic.dest_Trueprop qtrm
     val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
@@ -617,10 +607,10 @@
       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   in
     Drule.instantiate' []
-      [SOME (Thm.global_cterm_of thy rtrm'),
-       SOME (Thm.global_cterm_of thy reg_goal),
+      [SOME (Thm.cterm_of ctxt rtrm'),
+       SOME (Thm.cterm_of ctxt reg_goal),
        NONE,
-       SOME (Thm.global_cterm_of thy inj_goal)] procedure_thm
+       SOME (Thm.cterm_of ctxt inj_goal)] procedure_thm
   end
 
 
@@ -668,7 +658,6 @@
 
 fun partiality_procedure_inst ctxt rtrm qtrm =
   let
-    val thy = Proof_Context.theory_of ctxt
     val rtrm' = HOLogic.dest_Trueprop rtrm
     val qtrm' = HOLogic.dest_Trueprop qtrm
     val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
@@ -677,9 +666,9 @@
       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   in
     Drule.instantiate' []
-      [SOME (Thm.global_cterm_of thy reg_goal),
+      [SOME (Thm.cterm_of ctxt reg_goal),
        NONE,
-       SOME (Thm.global_cterm_of thy inj_goal)] partiality_procedure_thm
+       SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm
   end