equal
deleted
inserted
replaced
56 let |
56 let |
57 val initial = null (get_thmss ctxt); |
57 val initial = null (get_thmss ctxt); |
58 val (name, ctxt') = ML_Context.variant kind ctxt; |
58 val (name, ctxt') = ML_Context.variant kind ctxt; |
59 val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
59 val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
60 |
60 |
61 val ml_body = "Isabelle." ^ name; |
61 val ml_body = ML_Context.struct_name ctxt ^ "." ^ name; |
62 fun decl final_ctxt = |
62 fun decl final_ctxt = |
63 if initial then |
63 if initial then |
64 let |
64 let |
65 val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a); |
65 val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a); |
66 val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n"; |
66 val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n"; |