1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed Dec 14 14:20:25 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Sun Dec 18 16:27:41 2016 +0100
     1.3 @@ -120,12 +120,12 @@
     1.4        let 
     1.5          val cpI = if pI = e_pblID then pI' else pI;
     1.6    	    val cmI = if mI = e_metID then mI' else mI;
     1.7 -  	    val {ppc, prls, where_, ...} = get_pbt cpI;
     1.8 +  	    val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
     1.9    	    val pre = check_preconds "thy 100820" prls where_ probl;
    1.10    	    val pb = foldl and_ (true, map fst pre);
    1.11    	    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)
    1.12    	    val (_, tac) =
    1.13 -  	      Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
    1.14 +  	      Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
    1.15        in
    1.16          case tac of
    1.17    	      Apply_Method mI => 
    1.18 @@ -279,8 +279,8 @@
    1.19    	  if pI' = e_pblID 
    1.20    		then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
    1.21    		else pI'
    1.22 -  	val {ppc, where_, prls, ...} = get_pbt pblID
    1.23 -  	val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
    1.24 +  	val {ppc, where_, prls, ...} = Specify.get_pbt pblID
    1.25 +  	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
    1.26    in
    1.27      (model_ok, pblID, hdl, pbl, pre)
    1.28    end
    1.29 @@ -294,8 +294,8 @@
    1.30    	val metID = if mI' = e_metID 
    1.31    		    then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
    1.32    		    else mI'
    1.33 -  	val {ppc, pre, prls, scr, ...} = get_met metID
    1.34 -  	val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
    1.35 +  	val {ppc, pre, prls, scr, ...} = Specify.get_met metID
    1.36 +  	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
    1.37    in
    1.38      (model_ok, metID, scr, pbl, pre)
    1.39    end
    1.40 @@ -307,8 +307,8 @@
    1.41        case get_obj I pt p of
    1.42          PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
    1.43        | PrfObj _ => error "context_pbl: uncovered case"
    1.44 -  	val {ppc,where_,prls,...} = get_pbt pI
    1.45 -  	val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
    1.46 +  	val {ppc,where_,prls,...} = Specify.get_pbt pI
    1.47 +  	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
    1.48    in
    1.49      (model_ok, pI, hdl, pbl, pre)
    1.50    end
    1.51 @@ -319,8 +319,8 @@
    1.52        case get_obj I pt p of
    1.53          PblObj {meth, origin = (os, _, _),...} => (meth, os)
    1.54        | PrfObj _ => error "context_met: uncovered case"
    1.55 -  	val {ppc,pre,prls,scr,...} = get_met mI
    1.56 -  	val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
    1.57 +  	val {ppc,pre,prls,scr,...} = Specify.get_met mI
    1.58 +  	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
    1.59    in
    1.60      (model_ok, mI, scr, pbl, pre)
    1.61    end
    1.62 @@ -332,11 +332,11 @@
    1.63          PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
    1.64        | PrfObj _ => error "context_met: uncovered case"
    1.65    in
    1.66 -    case refine_pbl (assoc_thy "Isac") pI probl of
    1.67 +    case Specify.refine_pbl (assoc_thy "Isac") pI probl of
    1.68    	  NONE => (*copy from context_pbl*)
    1.69    	    let
    1.70 -  	      val {ppc,where_,prls,...} = get_pbt pI
    1.71 -  	      val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
    1.72 +  	      val {ppc,where_,prls,...} = Specify.get_pbt pI
    1.73 +  	      val (_, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
    1.74          in
    1.75            (false, pI, hdl, pbl, pre)
    1.76          end
    1.77 @@ -369,10 +369,11 @@
    1.78    in
    1.79      case form of
    1.80        Form t => Ctree.FormKF (term2str t)
    1.81 -    | ModSpec (_,p_, _, gfr, pre, _) => Ctree.PpcKF (
    1.82 +    | ModSpec (_, p_, _, gfr, pre, _) =>
    1.83 +      Ctree.PpcKF (
    1.84          (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method []
    1.85          | _ => error "TESTg_form: uncovered case",
    1.86 - 			itms2itemppc (assoc_thy"Isac") gfr pre))
    1.87 + 			Specify.itms2itemppc (assoc_thy"Isac") gfr pre))
    1.88     end
    1.89  
    1.90  (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;