1.1 --- a/src/Tools/isac/Specify/i-model.sml	Mon May 18 14:12:01 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Mon May 18 14:21:41 2020 +0200
     1.3 @@ -402,7 +402,7 @@
     1.4  fun complete' pbt (i, v, f, d, ts) =
     1.5    (i, v, true, f, Cor ((d, ts), ((snd o snd o the o (find_first (eq1 d))) pbt, ts)))
     1.6      handle _ => (i, v, true, f, Cor ((d, ts), (d, ts)))
     1.7 -      (*dsc in oris, but not in pbl pat list: keep this dsc*)
     1.8 +      (*descriptor in O_Model, but not in Problem_Pattern.T, thus keep this descriptor*)
     1.9  
    1.10  (* filter out oris which have same description in itms *)
    1.11  fun filter_outs oris [] = oris

     2.1 --- a/src/Tools/isac/Specify/o-model.sml	Mon May 18 14:12:01 2020 +0200
     2.2 +++ b/src/Tools/isac/Specify/o-model.sml	Mon May 18 14:21:41 2020 +0200
     2.3 @@ -229,10 +229,4 @@
     2.4  	  handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
     2.5    in (split_list o (map ori2fmz_vals)) oris end
     2.6  
     2.7 -(* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
     2.8 -fun vars_of_pbl_' pbl_ = 
     2.9 -  let
    2.10 -    fun var_of_pbl_ (_, (_, t)) = t: term
    2.11 -  in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
    2.12 -
    2.13  (**)end(**);
    2.14 \ No newline at end of file

     3.1 --- a/src/Tools/isac/Specify/p-spec.sml	Mon May 18 14:12:01 2020 +0200
     3.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Mon May 18 14:21:41 2020 +0200
     3.3 @@ -7,12 +7,14 @@
     3.4  
     3.5  signature PRESENTATION_SPECIFICATION =
     3.6  sig
     3.7 +(*/------- rename -------\*)
     3.8    datatype iitem =
     3.9        Find of TermC.as_string list
    3.10      | Given of TermC.as_string list
    3.11      | Relate of TermC.as_string list
    3.12    type imodel = iitem list
    3.13    type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
    3.14 +  val empty: icalhd
    3.15    val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
    3.16  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    3.17    (*  NONE *)
    3.18 @@ -36,6 +38,7 @@
    3.19      (''a * string) list ->
    3.20        (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
    3.21  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.22 +(*\------- rename -------/*)
    3.23  end
    3.24  
    3.25  (**)
    3.26 @@ -61,7 +64,7 @@
    3.27    imodel *           (* the model                          *)
    3.28    Pos.pos_ *         (* model belongs to Problem or Method *)
    3.29    References.T;      (* into Know_Store                    *)
    3.30 -val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
    3.31 +val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
    3.32  
    3.33  (* re-parse itms with a new thy and prepare for checking with ori list *)
    3.34  fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =

     4.1 --- a/src/Tools/isac/Specify/specify-step.sml	Mon May 18 14:12:01 2020 +0200
     4.2 +++ b/src/Tools/isac/Specify/specify-step.sml	Mon May 18 14:21:41 2020 +0200
     4.3 @@ -69,7 +69,7 @@
     4.4       end
     4.5    | check (Tactic.Specify_Method mID) _ =
     4.6        Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled later*)], [(*filled later*)]))
     4.7 -  | check (Tactic.Specify_Problem pID) (pt, (p, p_)) =
     4.8 +  | check (Tactic.Specify_Problem pID) (pt, (p, _)) =
     4.9        let
    4.10  		    val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
    4.11  		      Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}

     5.1 --- a/src/Tools/isac/Specify/step-specify.sml	Mon May 18 14:12:01 2020 +0200
     5.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Mon May 18 14:21:41 2020 +0200
     5.3 @@ -66,8 +66,7 @@
     5.4        val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
     5.5          PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
     5.6        | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
     5.7 -      val (dI, pI, mI) = References.select ospec spec
     5.8 -      val thy = ThyC.get_theory dI
     5.9 +      val (_, pI, mI) = References.select ospec spec
    5.10        val mpc = (#ppc o Method.from_store) mI (* just for reuse I_Model.complete_method *)
    5.11        val {cas, ppc, ...} = Problem.from_store pI
    5.12        val pbl = I_Model.init ppc (* fill in descriptions *)
    5.13 @@ -97,7 +96,6 @@
    5.14              val {met, ...} = Problem.from_store pI'
    5.15  	          (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
    5.16  	          val mI = if length met = 0 then Method.id_empty else hd met
    5.17 -            val thy = ThyC.get_theory dI
    5.18  	          val (pos, c, _, pt) = 
    5.19  		          Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
    5.20  	        in
    5.21 @@ -225,11 +223,10 @@
    5.22      (*WN110515 initialise ctxt again from itms and add preconds*)
    5.23    | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pt, pos as (p, _)) =
    5.24        let
    5.25 -        val (_, _, _, _, dI, _, ctxt, _) = case get_obj I pt p of
    5.26 +        val (_, _, _, _, _, _, ctxt, _) = case get_obj I pt p of
    5.27            PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
    5.28              (oris, dI', pI', mI', dI, mI, ctxt, met)
    5.29          | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
    5.30 -        val thy = ThyC.get_theory dI
    5.31          val (p, pt) =
    5.32            case  Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
    5.33              ((p, Pbl), _, _, pt) => (p, pt)