# HG changeset patch
# User wenzelm
# Date 932412393 -7200
# Node ID 3535eec33c5067c6f6c98a9a3f39141889521448
# Parent  d103b875ef1d9dc2b1471d182ad69ee74f551684
facts: no statement_binds;

diff -r d103b875ef1d -r 3535eec33c50 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Mon Jul 19 17:21:40 1999 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Mon Jul 19 21:26:33 1999 +0200
@@ -35,11 +35,8 @@
   | _ => []);
 
 fun facts _ [] = []
-  | facts name [prop] = statement_binds (name, prop) @ dddot_bind prop
-  | facts name props =
-      flat (map statement_binds
-        (map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props))) @
-      dddot_bind (Library.last_elem props);
+  | facts name [prop] = dddot_bind prop
+  | facts name props =  dddot_bind (Library.last_elem props);
       
 
 end;