src/Pure/Isar/auto_bind.ML
changeset 7452 c2289eabf706
parent 7331 aee8f76fe54c
child 7474 43cedde6d52a
equal deleted inserted replaced
7451:d643b3c4996a 7452:c2289eabf706
    36   (case Logic.strip_imp_concl prop of
    36   (case Logic.strip_imp_concl prop of
    37     Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    37     Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    38   | _ => []);
    38   | _ => []);
    39 
    39 
    40 fun facts _ [] = []
    40 fun facts _ [] = []
    41   | facts name [prop] = dddot_bind prop
    41   | facts name props =
    42   | facts name props =  dddot_bind (Library.last_elem props);
    42       let val prop = Library.last_elem props
       
    43       in dddot_bind prop @ statement_binds ("this", prop) end;
    43       
    44       
    44 
    45 
    45 end;
    46 end;