100 val example_id' = References_Def.explode_id example_id |
100 val example_id' = References_Def.explode_id example_id |
101 val (_, (fmz as (model, refs as (_(*thy_id*), probl_id, _)))) = |
101 val (_, (fmz as (model, refs as (_(*thy_id*), probl_id, _)))) = |
102 Store.get (KEStore_Elems.get_expls @{theory}) example_id' example_id' |
102 Store.get (KEStore_Elems.get_expls @{theory}) example_id' example_id' |
103 val ctxt = ContextC.initialise' thy model; |
103 val ctxt = ContextC.initialise' thy model; |
104 |
104 |
105 val o_model = Problem.from_store ctxt probl_id |> #ppc |> O_Model.init thy model |
105 val o_model = Problem.from_store ctxt probl_id |> #model |> O_Model.init thy model |
106 in |
106 in |
107 Ctree.Nd (Ctree.PblObj { |
107 Ctree.Nd (Ctree.PblObj { |
108 fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)), |
108 fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)), |
109 spec = References.empty, probl = I_Model.empty, meth = I_Model.empty, |
109 spec = References.empty, probl = I_Model.empty, meth = I_Model.empty, |
110 ctxt = ctxt, loc = (NONE, NONE), |
110 ctxt = ctxt, loc = (NONE, NONE), |