author | wenzelm |
Sat, 25 Oct 2014 11:53:35 +0200 | |
changeset 58782 | 7305bad408b5 |
parent 58781 | c385da5c665e |
child 58783 | c6348a062131 |
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Oct 24 20:49:23 2014 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Sat Oct 25 11:53:35 2014 +0200 @@ -316,7 +316,7 @@ SOME data => data | NONE => (error "lookup_pred_data: something went utterly wrong") -fun lives_of_fp fp_sugar = +fun lives_of_fp (fp_sugar: fp_sugar) = let val As = snd (dest_Type (#T fp_sugar)) val liveness = liveness_of_fp_bnf (length As) (hd (#bnfs (#fp_res fp_sugar)));