src/HOL/Tools/Transfer/transfer_bnf.ML
changeset 58782 7305bad408b5
parent 58722 9cd739562c71
child 58963 26bf09b95dda
--- 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)));