107 val pt = update_met pt [] mits |
107 val pt = update_met pt [] mits |
108 in ((pt, ([], Met)), []) end |
108 in ((pt, ([], Met)), []) end |
109 else (* new example, pepare for interactive modeling *) |
109 else (* new example, pepare for interactive modeling *) |
110 let |
110 let |
111 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) |
111 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) |
112 ([], Spec.empty_spec) ([], Spec.empty_spec, TermC.empty, ContextC.empty) |
112 ([], Spec.empty) ([], Spec.empty, TermC.empty, ContextC.empty) |
113 in ((pt, ([], Pbl)), []) end |
113 in ((pt, ([], Pbl)), []) end |
114 | nxt_specify_init_calc (fmz, (dI, pI, mI)) = |
114 | nxt_specify_init_calc (fmz, (dI, pI, mI)) = |
115 let (* both """"""""""""""""""""""""" either empty or complete *) |
115 let (* both """"""""""""""""""""""""" either empty or complete *) |
116 val thy = ThyC.get_theory dI |
116 val thy = ThyC.get_theory dI |
117 val (pI, (pors, pctxt), mI) = |
117 val (pI, (pors, pctxt), mI) = |