src/Pure/Isar/auto_bind.ML
changeset 7452 c2289eabf706
parent 7331 aee8f76fe54c
child 7474 43cedde6d52a
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Fri Sep 03 14:52:01 1999 +0200
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Fri Sep 03 14:52:19 1999 +0200
     1.3 @@ -38,8 +38,9 @@
     1.4    | _ => []);
     1.5  
     1.6  fun facts _ [] = []
     1.7 -  | facts name [prop] = dddot_bind prop
     1.8 -  | facts name props =  dddot_bind (Library.last_elem props);
     1.9 +  | facts name props =
    1.10 +      let val prop = Library.last_elem props
    1.11 +      in dddot_bind prop @ statement_binds ("this", prop) end;
    1.12        
    1.13  
    1.14  end;