| changeset 53143 | ba80154a1118 |
| parent 53138 | 4ef7d52cc5a0 |
| child 53203 | 222ea6acbdd6 |
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 22 16:03:13 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 22 17:13:46 2013 +0200 @@ -28,6 +28,7 @@ (*all BNFs have the same lives*) fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy = let + val time = time lthy; val timer = time (Timer.startRealTimer ()); val live = live_of_bnf (hd bnfs);