# HG changeset patch
# User wenzelm
# Date 1439662025 -7200
# Node ID b316f218ef348928bf9dec0618f5761d014ae19a
# Parent  51425cbe8ce9f1f616fbf477a7f92346d9f1c5bb
clarified context;

diff -r 51425cbe8ce9 -r b316f218ef34 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sat Aug 15 19:42:35 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sat Aug 15 20:07:05 2015 +0200
@@ -643,7 +643,7 @@
   @{index_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\
   @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
   @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
-  @{index_ML Thm.all: "cterm -> cterm -> cterm"} \\
+  @{index_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\
   @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
   \end{mldecls}
   \begin{mldecls}
diff -r 51425cbe8ce9 -r b316f218ef34 src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Sat Aug 15 19:42:35 2015 +0200
+++ b/src/Pure/Isar/subgoal.ML	Sat Aug 15 20:07:05 2015 +0200
@@ -114,9 +114,9 @@
           :
           C
 *)
-fun lift_subgoals params asms th =
+fun lift_subgoals ctxt params asms th =
   let
-    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
+    fun lift ct = fold_rev (Thm.all_name ctxt) params (Drule.list_implies (asms, ct));
     val unlift =
       fold (Thm.elim_implies o Thm.assume) asms o
       Drule.forall_elim_list (map #2 params) o Thm.assume;
@@ -129,7 +129,7 @@
     val idx = Thm.maxidx_of st0 + 1;
     val ps = map #2 params;
     val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
-    val (subgoals, st3) = lift_subgoals params asms st2;
+    val (subgoals, st3) = lift_subgoals ctxt2 params asms st2;
     val result = st3
       |> Goal.conclude
       |> Drule.implies_intr_list asms
diff -r 51425cbe8ce9 -r b316f218ef34 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Aug 15 19:42:35 2015 +0200
+++ b/src/Pure/more_thm.ML	Sat Aug 15 20:07:05 2015 +0200
@@ -23,8 +23,8 @@
   val aconvc: cterm * cterm -> bool
   val add_frees: thm -> cterm list -> cterm list
   val add_vars: thm -> cterm list -> cterm list
-  val all_name: string * cterm -> cterm -> cterm
-  val all: cterm -> cterm -> cterm
+  val all_name: Proof.context -> string * cterm -> cterm -> cterm
+  val all: Proof.context -> cterm -> cterm -> cterm
   val mk_binop: cterm -> cterm -> cterm -> cterm
   val dest_binop: cterm -> cterm * cterm
   val dest_implies: cterm -> cterm * cterm
@@ -120,16 +120,13 @@
 
 (* cterm constructors and destructors *)
 
-fun all_name (x, t) A =
+fun all_name ctxt (x, t) A =
   let
-    val thy = Thm.theory_of_cterm t;
     val T = Thm.typ_of_cterm t;
-  in
-    Thm.apply (Thm.global_cterm_of thy (Const ("Pure.all", (T --> propT) --> propT)))
-      (Thm.lambda_name (x, t) A)
-  end;
+    val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT));
+  in Thm.apply all_const (Thm.lambda_name (x, t) A) end;
 
-fun all t A = all_name ("", t) A;
+fun all ctxt t A = all_name ctxt ("", t) A;
 
 fun mk_binop c a b = Thm.apply (Thm.apply c a) b;
 fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);