src/Pure/Isar/auto_bind.ML
changeset 7048 3535eec33c50
parent 6796 c2e5cb8cd50d
child 7331 aee8f76fe54c
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Mon Jul 19 17:21:40 1999 +0200
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Mon Jul 19 21:26:33 1999 +0200
     1.3 @@ -35,11 +35,8 @@
     1.4    | _ => []);
     1.5  
     1.6  fun facts _ [] = []
     1.7 -  | facts name [prop] = statement_binds (name, prop) @ dddot_bind prop
     1.8 -  | facts name props =
     1.9 -      flat (map statement_binds
    1.10 -        (map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props))) @
    1.11 -      dddot_bind (Library.last_elem props);
    1.12 +  | facts name [prop] = dddot_bind prop
    1.13 +  | facts name props =  dddot_bind (Library.last_elem props);
    1.14        
    1.15  
    1.16  end;