title: Isabelle: locale interpration about record fails in proof
body: <p>Using the Algebra library, I encountered the following problem. In a proof I wanted to interpret the additive structure of a ring as a group. Here is a sample code:</p>
  
  <pre><code>theory aaa
  imports "~~/src/HOL/Algebra/Ring"
  begin
  
  lemma assumes "ring R"
  shows "True"
  proof-
  interpret ring R by fact
  interpret additive: comm_group "⦇carrier = carrier R, mult = add R, one = zero R⦈" by(unfold_locales)
  </code></pre>
  
  <p>But I can't access the facts from the group locale. Typing</p>
  
  <pre><code>thm additive.m_assoc
  </code></pre>
  
  <p>gives the message "Undefined fact". However, it works when I define the additive structure with the monoid.make command:</p>
  
  <pre><code>interpret additivee: comm_group "monoid.make (carrier R) (add R) (zero R)" sorry
  
  thm additivee.m_assoc
  </code></pre>
  
  <p>It also works if I try to do the same for the multiplicative structure, or if I remove</p>
  
  <pre><code>interpret ring R by fact
  </code></pre>
  
  <p>Any ideas about what's going on?</p>