--- 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;