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;