'write': actually observe the proof structure (like 'let' or 'fix');

--- a/src/Pure/Isar/proof.ML	Thu Apr 29 17:15:23 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Apr 29 17:29:53 2010 +0200
@@ -545,8 +545,10 @@
 
 local
 
-fun gen_write prep_arg mode args = map_context (fn ctxt =>
-  ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args));
+fun gen_write prep_arg mode args =
+  assert_forward
+  #> map_context (fn ctxt => ctxt |> ProofContext.notation true mode (map (prep_arg ctxt) args))
+  #> put_facts NONE;
 
 in