diff -r 50c5b0912a0c -r 3702086a15a3 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Wed Jun 13 00:01:41 2007 +0200
+++ b/src/Pure/Tools/class_package.ML	Wed Jun 13 00:01:51 2007 +0200
@@ -371,13 +371,13 @@
 fun prove_interpretation tac prfx_atts expr insts thy =
   thy
   |> Locale.interpretation_i I prfx_atts expr insts
-  |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
+  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   |> ProofContext.theory_of;
 
 fun prove_interpretation_in tac after_qed (name, expr) thy =
   thy
   |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr)
-  |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
+  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   |> ProofContext.theory_of;
 
 fun instance_sort' do_proof (class, sort) theory =