src/Tools/isac/Interpret/appl.sml
changeset 59271 7a02202e4577
parent 59269 1da53d1540fe
child 59272 1d3ef477d9c8
     1.1 --- a/src/Tools/isac/Interpret/appl.sml	Mon Dec 19 09:02:41 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Mon Dec 19 10:37:44 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,...} = Specify.get_pbt pI'
     1.7 -	        val pbl = Ctree.init_pbl ppc
     1.8 +	        val pbl = Generate.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 @@ -316,7 +316,7 @@
    1.13  	val thy = assoc_thy (if dI' = e_domID then dI else dI');
    1.14          val {ppc,where_,prls,...} = Specify.get_pbt pID;
    1.15  	val pbl = if pI'=e_pblID andalso pI=e_pblID
    1.16 -		  then (false, (Ctree.init_pbl ppc, []))
    1.17 +		  then (false, (Generate.init_pbl ppc, []))
    1.18  		  else Specify.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;