# HG changeset patch
# User wenzelm
# Date 936363139 -7200
# Node ID c2289eabf706bedb4d71427dd838c828c4a43795
# Parent  d643b3c4996aa8afa2427533c96195fa11f8fddb
"this";

diff -r d643b3c4996a -r c2289eabf706 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Fri Sep 03 14:52:01 1999 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Fri Sep 03 14:52:19 1999 +0200
@@ -38,8 +38,9 @@
   | _ => []);
 
 fun facts _ [] = []
-  | facts name [prop] = dddot_bind prop
-  | facts name props =  dddot_bind (Library.last_elem props);
+  | facts name props =
+      let val prop = Library.last_elem props
+      in dddot_bind prop @ statement_binds ("this", prop) end;
       
 
 end;