# HG changeset patch
# User wenzelm
# Date 1438102630 -7200
# Node ID c93a83472eab060df40a6e11c0095c7df6fa421b
# Parent  9372f29acd47b2854f6e193535881029a6719e5c
clarified context;

diff -r 9372f29acd47 -r c93a83472eab src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Tue Jul 28 18:27:39 2015 +0200
+++ b/src/Pure/conjunction.ML	Tue Jul 28 18:57:10 2015 +0200
@@ -138,8 +138,13 @@
 
 local
 
-fun conjs thy n =
-  let val As = map (fn A => Thm.global_cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n)
+val bootstrap_thy = Context.theory_of (Context.the_thread_data ());
+
+fun conjs n =
+  let
+    val As =
+      map (fn A => Thm.global_cterm_of bootstrap_thy (Free (A, propT)))
+        (Name.invent Name.context "A" n);
   in (As, mk_conjunction_balanced As) end;
 
 val B = read_prop "B";
@@ -159,8 +164,7 @@
   if n < 2 then th
   else
     let
-      val thy = Thm.theory_of_thm th;
-      val (As, C) = conjs thy n;
+      val (As, C) = conjs n;
       val D = Drule.mk_implies (C, B);
     in
       comp_rule th
@@ -177,8 +181,7 @@
   if n < 2 then th
   else
     let
-      val thy = Thm.theory_of_thm th;
-      val (As, C) = conjs thy n;
+      val (As, C) = conjs n;
       val D = Drule.list_implies (As, B);
     in
       comp_rule th