src/Doc/Implementation/Proof.thy

--- a/src/Doc/Implementation/Proof.thy	Tue Oct 28 11:42:51 2014 +0100
+++ b/src/Doc/Implementation/Proof.thy	Tue Oct 28 13:52:54 2014 +0100
@@ -463,7 +463,8 @@
         Subgoal.focus goal_ctxt 1 goal;
       val [A, B] = #prems focus;
       val [(_, x)] = #params focus;\<close>
-    oops
+    sorry
+end
 
 text \<open>\medskip The next example demonstrates forward-elimination in
   a local context, using @{ML Obtain.result}.\<close>