src/Tools/isac/Interpret/appl.sml
changeset 59266 56762e8a672e
parent 59265 ee68ccda7977
child 59269 1da53d1540fe
     1.1 --- a/src/Tools/isac/Interpret/appl.sml	Mon Dec 12 18:08:13 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Wed Dec 14 09:37:01 2016 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4          let 
     1.5            val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
     1.6  	        val {ppc,...} = get_pbt pI'
     1.7 -	        val pbl = init_pbl ppc
     1.8 +	        val pbl = Ctree.init_pbl ppc
     1.9          in Chead.Appl (Model_Problem' (pI', pbl, [])) end
    1.10  
    1.11    | applicable_in (p,p_) pt (Refine_Tacitly pI) = 
    1.12 @@ -318,7 +318,7 @@
    1.13  	val thy = assoc_thy (if dI' = e_domID then dI else dI');
    1.14          val {ppc,where_,prls,...} = get_pbt pID;
    1.15  	val pbl = if pI'=e_pblID andalso pI=e_pblID
    1.16 -		  then (false, (init_pbl ppc, []))
    1.17 +		  then (false, (Ctree.init_pbl ppc, []))
    1.18  		  else match_itms_oris thy itms (ppc,where_,prls) oris;
    1.19      in Chead.Appl (Specify_Problem' (pID, pbl)) end
    1.20  (* val Specify_Method mID = nxt; val (p,p_) = p;