src/Pure/Isar/element.ML

     (K (ALLGOALS
       (PRECISE_CONJUNCTS ~1 (ALLGOALS
         (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))));
 
 fun pretty_witness ctxt witn =
-  let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt
-  in
+  let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt in
     Pretty.block (prt_term (witness_prop witn) ::
       (if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
          (map prt_term (witness_hyps witn))] else []))
   end;
 

   if Symtab.is_empty env then th
   else
     let val subst = instT_subst env th
     in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
 
-fun instT_morphism thy env = Morphism.morphism
-  {name = I, var = I, typ = instT_type env, term = instT_term env, fact = map (instT_thm thy env)};
+fun instT_morphism thy env =
+  let val thy_ref = Theory.self_ref thy in
+    Morphism.morphism
+     {name = I, var = I,
+      typ = instT_type env,
+      term = instT_term env,
+      fact = map (fn th => instT_thm (Theory.deref thy_ref) env th)}
+  end;
 
 
 (* instantiate types and terms *)
 
 fun inst_term (envT, env) =

        (instantiate_tfrees thy substT #>
         instantiate_frees thy subst #>
         Drule.fconv_rule (Thm.beta_conversion true))
     end;
 
-fun inst_morphism thy envs = Morphism.morphism
-  {name = I, var = I, typ = instT_type (#1 envs), term = inst_term envs,
-    fact = map (inst_thm thy envs)};
+fun inst_morphism thy envs =
+  let val thy_ref = Theory.self_ref thy in
+    Morphism.morphism
+     {name = I, var = I,
+      typ = instT_type (#1 envs),
+      term = inst_term envs,
+      fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)}
+  end;
 
 
 (* satisfy hypotheses *)
 
 fun satisfy_thm witns thm = thm |> fold (fn hyp =>