src/Pure/Isar/class.ML
changeset 28259 5b2af04ec9fb
parent 28110 9d121b171a0a
child 28666 d2dbfe3a0284
     1.1 --- a/src/Pure/Isar/class.ML	Wed Sep 17 11:42:25 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Sep 17 15:21:30 2008 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  (** auxiliary **)
     1.5  
     1.6  fun prove_interpretation tac prfx_atts expr inst =
     1.7 -  Locale.interpretation_i I prfx_atts expr inst
     1.8 +  Locale.interpretation_i I prfx_atts expr inst #> snd
     1.9    #> Proof.global_terminal_proof
    1.10        (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
    1.11    #> ProofContext.theory_of;