src/Tools/isac/Interpret/calchead.sml
branchdecompose-isar
changeset 42004 c80b4f89b025
parent 41994 54d8032d66fb
child 42005 906647153d9a
     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),