# HG changeset patch
# User wenzelm
# Date 1272554993 -7200
# Node ID c966a1aab8608048deca8cbca63369039fb7a85f
# Parent  6b56e679d9ffb0c08a081a1fd1433f1050d7ecf4
'write': actually observe the proof structure (like 'let' or 'fix');

diff -r 6b56e679d9ff -r c966a1aab860 src/Pure/Isar/proof.ML
--- 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