# HG changeset patch
# User wenzelm
# Date 1433152045 -7200
# Node ID 68699e576d515fefbd2b0e5c032ee9194d94850a
# Parent  6fc771cb42eb6cc2d93c1d79a50ffae6268470e7
tuned;

diff -r 6fc771cb42eb -r 68699e576d51 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Jun 01 11:46:03 2015 +0200
+++ b/src/HOL/Tools/record.ML	Mon Jun 01 11:47:25 2015 +0200
@@ -169,10 +169,9 @@
   resolve_from_net_tac ctxt iso_tuple_intros THEN'
   CSUBGOAL (fn (cgoal, i) =>
     let
-      val thy = Thm.theory_of_cterm cgoal;
       val goal = Thm.term_of cgoal;
 
-      val isthms = Iso_Tuple_Thms.get thy;
+      val isthms = Iso_Tuple_Thms.get (Proof_Context.theory_of ctxt);
       fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
 
       val goal' = Envir.beta_eta_contract goal;