| changeset 22658 | 263d42253f53 |
| parent 22588 | 4a859d13ef83 |
| child 22737 | d87ccbcc2702 |
--- a/src/Pure/Tools/class_package.ML Fri Apr 13 10:00:04 2007 +0200 +++ b/src/Pure/Tools/class_package.ML Fri Apr 13 10:01:43 2007 +0200 @@ -393,7 +393,7 @@ fun prove_interpretation tac prfx_atts expr insts thy = thy - |> Locale.interpretation_i I prfx_atts expr insts + |> Locale.interpretation_i I prfx_atts expr (insts, []) |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) |> ProofContext.theory_of;