src/Pure/Isar/class.ML

--- a/src/Pure/Isar/class.ML	Wed Sep 17 11:42:25 2008 +0200
+++ b/src/Pure/Isar/class.ML	Wed Sep 17 15:21:30 2008 +0200
@@ -63,7 +63,7 @@
 (** auxiliary **)
 
 fun prove_interpretation tac prfx_atts expr inst =
-  Locale.interpretation_i I prfx_atts expr inst
+  Locale.interpretation_i I prfx_atts expr inst #> snd
   #> Proof.global_terminal_proof
       (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
   #> ProofContext.theory_of;