equal
deleted
inserted
replaced
274 xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct, |
274 xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct, |
275 dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts}; |
275 dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts}; |
276 |
276 |
277 fun time ctxt timer msg = (if Config.get ctxt bnf_timing |
277 fun time ctxt timer msg = (if Config.get ctxt bnf_timing |
278 then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ |
278 then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ |
279 "ms") |
279 " ms") |
280 else (); Timer.startRealTimer ()); |
280 else (); Timer.startRealTimer ()); |
281 |
281 |
282 val preN = "pre_" |
282 val preN = "pre_" |
283 val rawN = "raw_" |
283 val rawN = "raw_" |
284 |
284 |