equal
deleted
inserted
replaced
357 fun print_code is_first const ctxt = |
357 fun print_code is_first const ctxt = |
358 let |
358 let |
359 val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; |
359 val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; |
360 val (ml_code, consts_map) = Lazy.force acc_code; |
360 val (ml_code, consts_map) = Lazy.force acc_code; |
361 val ml_code = if is_first then ml_code else ""; |
361 val ml_code = if is_first then ml_code else ""; |
362 val body = "Isabelle." ^ the (AList.lookup (op =) consts_map const); |
362 val body = ML_Context.struct_name ctxt ^ "." ^ the (AList.lookup (op =) consts_map const); |
363 in (ml_code, body) end; |
363 in (ml_code, body) end; |
364 |
364 |
365 in |
365 in |
366 |
366 |
367 fun ml_code_antiq raw_const ctxt = |
367 fun ml_code_antiq raw_const ctxt = |