print_interps shows interpretations in proofs.

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jul 31 21:14:20 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jul 31 21:14:20 2010 +0200
@@ -729,8 +729,7 @@
       show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
         by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
     qed
-    print_interps logic_o  (* FIXME *)
-    thm loc.lor_o_def por_eq
+    print_interps logic_o
     have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
   }
 qed

--- a/src/Pure/Isar/isar_cmd.ML	Sat Jul 31 21:14:20 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -365,7 +365,7 @@
 
 fun print_registrations name = Toplevel.unknown_context o
   Toplevel.keep (fn state =>
-    Locale.print_registrations (Toplevel.theory_of state) name);
+    Locale.print_registrations (Toplevel.context_of state) name);
 
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);

--- a/src/Pure/Isar/locale.ML	Sat Jul 31 21:14:20 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Jul 31 21:14:20 2010 +0200
@@ -77,7 +77,7 @@
   val all_locales: theory -> string list
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> xstring -> unit
-  val print_registrations: theory -> string -> unit
+  val print_registrations: Proof.context -> string -> unit
   val locale_deps: theory ->
     { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
       * term list list Symtab.table Symtab.table
@@ -600,11 +600,15 @@
     |> Pretty.writeln
   end;
 
-fun print_registrations thy raw_name =
-  (case registrations_of_locale (Context.Theory thy) (intern thy raw_name) of
-      [] => Pretty.str ("no interpretations")
-    | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
-  |> Pretty.writeln;
+fun print_registrations ctxt raw_name =
+  let
+    val thy = ProofContext.theory_of ctxt;
+  in
+    (case registrations_of_locale  (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
+        [] => Pretty.str ("no interpretations")
+      | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
+    |> Pretty.writeln
+  end;
 
 fun locale_deps thy =
   let