diff -r 1fac64bbdb4f -r 7a0b8debef77 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Nov 08 08:56:24 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Nov 08 11:44:37 2011 +0100
@@ -64,7 +64,7 @@
 
 (*rewrite conclusion with k-th assumtion*)
 fun rewrite_with_asm_tac ctxt k =
-  Subgoal.FOCUS (fn {context=ctxt', prems, ...} =>
+  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
     Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
 
 fun dest_case thy t =