diff -r e43d761a742d -r 1a5dde5079ac src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/context.ML	Wed Sep 30 22:20:58 2009 +0200
@@ -455,7 +455,7 @@
 
 fun init_proof thy = Prf (init_data thy, check_thy thy);
 
-fun transfer_proof thy' (prf as Prf (data, thy_ref)) =
+fun transfer_proof thy' (Prf (data, thy_ref)) =
   let
     val thy = deref thy_ref;
     val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";