1.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml	Tue May 12 17:42:29 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml	Wed May 13 11:34:05 2020 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4    		then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
     1.5    		else pI'
     1.6    	val {ppc, where_, prls, ...} = Problem.from_store pblID
     1.7 -  	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
     1.8 +  	val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
     1.9    in
    1.10      (model_ok, pblID, hdl, pbl, pre)
    1.11    end
    1.12 @@ -163,7 +163,7 @@
    1.13    		    then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
    1.14    		    else mI'
    1.15    	val {ppc, pre, prls, scr, ...} = Method.from_store metID
    1.16 -  	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
    1.17 +  	val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
    1.18    in
    1.19      (model_ok, metID, scr, pbl, pre)
    1.20    end
    1.21 @@ -176,7 +176,7 @@
    1.22          Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
    1.23        | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
    1.24    	val {ppc,where_,prls,...} = Problem.from_store pI
    1.25 -  	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
    1.26 +  	val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
    1.27    in
    1.28      (model_ok, pI, hdl, pbl, pre)
    1.29    end
    1.30 @@ -188,7 +188,7 @@
    1.31          Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
    1.32        | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
    1.33    	val {ppc,pre,prls,scr,...} = Method.from_store mI
    1.34 -  	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
    1.35 +  	val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
    1.36    in
    1.37      (model_ok, mI, scr, pbl, pre)
    1.38    end
    1.39 @@ -204,7 +204,7 @@
    1.40    	  NONE => (*copy from context_pbl*)
    1.41    	    let
    1.42    	      val {ppc,where_,prls,...} = Problem.from_store pI
    1.43 -  	      val (_, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
    1.44 +  	      val (_, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
    1.45          in
    1.46            (false, pI, hdl, pbl, pre)
    1.47          end