1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed May 18 09:32:26 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed May 18 09:37:35 2011 +0200
1.3 @@ -1015,7 +1015,7 @@
1.4 "#Given" => Add_Given' (ct, met')
1.5 | "#Find" => Add_Find' (ct, met')
1.6 | "#Relate"=> Add_Relation'(ct, met'))
1.7 - (Uistate, e_ctxt) (p, Met) pt
1.8 + (Uistate, ctxt) (p, Met) pt
1.9 val pre' = check_preconds thy prls pre met'
1.10 val pb = foldl and_ (true, map fst pre')
1.11 val (p_, nxt) =
1.12 @@ -1053,7 +1053,7 @@
1.13 "#Given" => Add_Given' (ct, pbl')
1.14 | "#Find" => Add_Find' (ct, pbl')
1.15 | "#Relate"=> Add_Relation'(ct, pbl'))
1.16 - (Uistate, e_ctxt) (p,Pbl) pt
1.17 + (Uistate, ctxt) (p,Pbl) pt
1.18 val pre = check_preconds thy prls where_ pbl'
1.19 val pb = foldl and_ (true, map fst pre)
1.20 val (p_, nxt) =
1.21 @@ -1103,14 +1103,14 @@
1.22 (*ONLY for STARTING modeling phase*)
1.23 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1.24 let
1.25 - val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ...}) = get_obj I pt p
1.26 + val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ctxt, ...}) = get_obj I pt p
1.27 val thy' = if dI = e_domID then dI' else dI
1.28 val thy = assoc_thy thy'
1.29 val {ppc,prls,where_,...} = get_pbt pI'
1.30 val pre = check_preconds thy prls where_ pbl
1.31 val pb = foldl and_ (true, map fst pre)
1.32 val ((p,_),_,_,pt) =
1.33 - generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1.34 + generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.35 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.36 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.37 in ((p, Pbl), ((p, p_), Uistate),