1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Mon May 04 16:47:32 2020 +0200
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Mon May 04 17:08:32 2020 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4        string
     1.5      val keref2xml : int -> Specify.ketype -> Specify.kestoreID -> xml
     1.6      val model2xml :
     1.7 -       int -> Model.itm list -> (bool * Term.term) list -> xml
     1.8 +       int -> I_Model.T -> (bool * Term.term) list -> xml
     1.9      val modspec2xml : int -> Ctree.ocalhd -> xml
    1.10      val pattern2xml :
    1.11         int ->

     2.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Mon May 04 16:47:32 2020 +0200
     2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Mon May 04 17:08:32 2020 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4    | Not_Associated;
     2.5    val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
     2.6    
     2.7 -  val init_pstate: Rule_Set.T -> Proof.context -> Model.itm list -> Method.id ->
     2.8 +  val init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> Method.id ->
     2.9      Istate.T * Proof.context * Program.T
    2.10    val resume_prog: ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree -> 
    2.11      (Istate.T * Proof.context) * Program.T
    2.12 @@ -30,7 +30,7 @@
    2.13  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    2.14    (*NONE*)
    2.15  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    2.16 -  val arguments_from_model : Method.id -> Model.itm list -> term list
    2.17 +  val arguments_from_model : Method.id -> I_Model.T -> term list
    2.18  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.19  end 
    2.20  

     3.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml	Mon May 04 16:47:32 2020 +0200
     3.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml	Mon May 04 17:08:32 2020 +0200
     3.3 @@ -10,14 +10,14 @@
     3.4    val autocalc : Pos.pos' list -> Pos.pos' -> Calc.T * State_Steps.T ->
     3.5      Solve.auto -> string * Pos.pos' list * Calc.T
     3.6  
     3.7 -  val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
     3.8 -  val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list
     3.9 -  val context_met : Method.id -> Ctree.ctree -> Pos.pos -> bool * Method.id * Program.T * Model.itm list * (bool * term) list
    3.10 -  val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * Model.itm list * (bool * term) list
    3.11 +  val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * I_Model.T * (bool * term) list
    3.12 +  val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T * (bool * term) list
    3.13 +  val context_met : Method.id -> Ctree.ctree -> Pos.pos -> bool * Method.id * Program.T * I_Model.T * (bool * term) list
    3.14 +  val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * I_Model.T * (bool * term) list
    3.15    val set_method : Method.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    3.16    val set_problem : Problem.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    3.17    val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    3.18 -  val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * Model.itm list * (bool * term) list
    3.19 +  val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T * (bool * term) list
    3.20  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    3.21    (*NONE*)
    3.22  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

     4.1 --- a/src/Tools/isac/Specify/calchead.sml	Mon May 04 16:47:32 2020 +0200
     4.2 +++ b/src/Tools/isac/Specify/calchead.sml	Mon May 04 17:08:32 2020 +0200
     4.3 @@ -69,16 +69,16 @@
     4.4    type calcstate
     4.5    type calcstate'
     4.6  
     4.7 -  val nxt_spec : Pos.pos_ -> bool -> Model.ori list -> Spec.T -> Model.itm list * Model.itm list ->
     4.8 +  val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> Spec.T -> I_Model.T * I_Model.T ->
     4.9      (string * (term * 'a)) list * (string * (term * 'b)) list -> Spec.T -> Pos.pos_ * Tactic.input
    4.10  
    4.11    val reset_calchead : Calc.T -> Calc.T
    4.12    val get_ocalhd : Calc.T -> Ctree.ocalhd
    4.13 -  val ocalhd_complete : Model.itm list -> (bool * term) list -> ThyC.id * Problem.id * Method.id -> bool
    4.14 +  val ocalhd_complete : I_Model.T -> (bool * term) list -> ThyC.id * Problem.id * Method.id -> bool
    4.15    val all_modspec : Calc.T -> Calc.T 
    4.16  
    4.17 -  val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> Celem4.pat list -> Model.itm list
    4.18 -  val insert_ppc' : Model.itm -> Model.itm list -> Model.itm list
    4.19 +  val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Celem4.pat list -> I_Model.T
    4.20 +  val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T
    4.21  
    4.22    val complete_mod : Calc.T -> Calc.T
    4.23    val is_complete_mod : Calc.T -> bool
    4.24 @@ -91,21 +91,21 @@
    4.25    val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list 
    4.26    val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list
    4.27  
    4.28 -  val match_ags : theory -> Celem4.pat list -> term list -> Model.ori list
    4.29 +  val match_ags : theory -> Celem4.pat list -> term list -> O_Model.T
    4.30    val match_ags_msg : Problem.id -> term -> term list -> unit
    4.31 -  val oris2fmz_vals : Model.ori list -> string list * term list
    4.32 +  val oris2fmz_vals : O_Model.T -> string list * term list
    4.33    val vars_of_pbl_' : ('a * ('b * term)) list -> term list
    4.34 -  val is_known : Proof.context -> string -> Model.ori list -> term -> string * Model.ori * term list
    4.35 -  val is_notyet_input : Proof.context -> Model.itm list -> term list -> Model.ori -> ('a * (term * term)) list
    4.36 -    -> string * Model.itm
    4.37 +  val is_known : Proof.context -> string -> O_Model.T -> term -> string * O_Model.single * term list
    4.38 +  val is_notyet_input : Proof.context -> I_Model.T -> term list -> O_Model.single -> ('a * (term * term)) list
    4.39 +    -> string * I_Model.single
    4.40    val ppc2list : 'a Model.ppc -> 'a list
    4.41    val mk_delete: theory -> string -> Model.itm_ -> Tactic.input
    4.42    val mk_additem: string -> TermC.as_string -> Tactic.input
    4.43 -  val nxt_add: theory -> Model.ori list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
    4.44 +  val nxt_add: theory -> O_Model.T -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
    4.45    val is_error: Model.itm_ -> bool
    4.46 -  val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * Model.itm list -> Model.itm list * Model.itm list
    4.47 +  val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * I_Model.T -> I_Model.T * I_Model.T
    4.48    val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
    4.49 -  val vals_of_oris : Model.ori list -> term list
    4.50 +  val vals_of_oris : O_Model.T -> term list
    4.51    val specify_additem: string -> TermC.as_string -> Calc.T -> string * calcstate'
    4.52  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    4.53    val e_calcstate : Calc.T * State_Steps.T
    4.54 @@ -117,19 +117,19 @@
    4.55    val is_copy_named_generating_idstr : string -> bool
    4.56    val is_copy_named_generating : 'a * ('b * term) -> bool
    4.57    val is_copy_named : 'a * ('b * term) -> bool
    4.58 -  val ori2Coritm : Celem4.pat list -> Model.ori -> Model.itm
    4.59 +  val ori2Coritm : Celem4.pat list -> O_Model.single -> I_Model.single
    4.60    val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list
    4.61    val mtc : theory -> Celem4.pat -> term -> Model.preori option
    4.62    val cpy_nam : Celem4.pat list -> Model.preori list -> Celem4.pat -> Model.preori
    4.63 -  datatype additm = Add of Model.itm | Err of string
    4.64 -  val appl_add: Proof.context -> string -> Model.ori list ->
    4.65 -    Model.itm list -> (string * (term * term)) list -> TermC.as_string -> additm
    4.66 +  datatype additm = Add of I_Model.single | Err of string
    4.67 +  val appl_add: Proof.context -> string -> O_Model.T ->
    4.68 +    I_Model.T -> (string * (term * term)) list -> TermC.as_string -> additm
    4.69    val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
    4.70  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.71  
    4.72  (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
    4.73    val variants_in : term list -> int
    4.74 -  val is_untouched : Model.itm -> bool
    4.75 +  val is_untouched : I_Model.single -> bool
    4.76    val is_list_type : typ -> bool
    4.77    val parse_ok : Model.itm_ list -> bool
    4.78    val all_dsc_in : Model.itm_ list -> term list
    4.79 @@ -183,7 +183,7 @@
    4.80  
    4.81  (* is the calchead complete ? *)
    4.82  fun ocalhd_complete its pre (dI, pI, mI) = 
    4.83 -  foldl and_ (true, map #3 (its: Model.itm list)) andalso 
    4.84 +  foldl and_ (true, map #3 (its: I_Model.T)) andalso 
    4.85    foldl and_ (true, map #1 (pre: (bool * term) list)) andalso 
    4.86    dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
    4.87  
    4.88 @@ -230,7 +230,7 @@
    4.89  
    4.90  (* find_first item with #1 equal to id *)
    4.91  fun seek_ppc _ [] = NONE
    4.92 -  | seek_ppc id (p :: ppc) = if id = #1 (p: Model.itm) then SOME p else seek_ppc id ppc
    4.93 +  | seek_ppc id (p :: ppc) = if id = #1 (p: I_Model.single) then SOME p else seek_ppc id ppc
    4.94  
    4.95  fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
    4.96    gis @ whs @ fis @ wis @ res
    4.97 @@ -311,11 +311,11 @@
    4.98      end
    4.99    | nxt_add thy oris _ itms =
   4.100      let
   4.101 -      fun testr_vt v ori = member op= (#2 (ori : Model.ori)) v andalso (#3 ori) <> "#undef"
   4.102 -      fun testi_vt v itm = member op= (#2 (itm : Model.itm)) v
   4.103 -      fun test_id ids r = member op= ids (#1 (r : Model.ori))
   4.104 +      fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
   4.105 +      fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
   4.106 +      fun test_id ids r = member op= ids (#1 (r : O_Model.single))
   4.107        fun test_subset itm (_, _, _, d, ts) = 
   4.108 -        (Model.d_in (#5 (itm: Model.itm))) = d andalso subset op = (Model.ts_in (#5 itm), ts)
   4.109 +        (Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (Model.ts_in (#5 itm), ts)
   4.110        fun false_and_not_Sup (_, _, false, _, Model.Sup _) = false
   4.111          | false_and_not_Sup (_, _, false, _, _) = true
   4.112          | false_and_not_Sup _ = false
   4.113 @@ -491,7 +491,7 @@
   4.114  
   4.115  
   4.116  datatype additm =
   4.117 -	Add of Model.itm   (* return-value of appl_add *)
   4.118 +	Add of I_Model.single   (* return-value of appl_add *)
   4.119  | Err of string       (* error-message            *)
   4.120  
   4.121  (* add an item to the model; check wrt. oris and pbt.
   4.122 @@ -878,7 +878,7 @@
   4.123     if mI = Method.id_empty then omI else mI)
   4.124  
   4.125  (* get the values from oris; handle the term list w.r.t. penv *)
   4.126 -fun vals_of_oris (oris: Model.ori list) =
   4.127 +fun vals_of_oris (oris: O_Model.T) =
   4.128    ((map (Model.mkval' o (#5))) o 
   4.129      (filter ((member_swap op= 1) o (#2)))) oris
   4.130  

     5.1 --- a/src/Tools/isac/Specify/generate.sml	Mon May 04 16:47:32 2020 +0200
     5.2 +++ b/src/Tools/isac/Specify/generate.sml	Mon May 04 17:08:32 2020 +0200
     5.3 @@ -11,12 +11,12 @@
     5.4    | Error' of string
     5.5    | FormKF of TermC.as_string
     5.6    | PpcKF of pblmet * Model.item Model.ppc
     5.7 -  | RefinedKF of Problem.id * (Model.itm list * (bool * term) list)
     5.8 +  | RefinedKF of Problem.id * (I_Model.T * (bool * term) list)
     5.9  
    5.10    type test_out = Pos.pos' * Pos.pos' list * mout * Ctree.ctree
    5.11  
    5.12 -  val init_pbl: (string * (term * 'a)) list -> Model.itm list
    5.13 -  val init_pbl': (string * (term * term)) list -> Model.itm list
    5.14 +  val init_pbl: (string * (term * 'a)) list -> I_Model.T
    5.15 +  val init_pbl': (string * (term * term)) list -> I_Model.T
    5.16    val generate_inconsistent_rew: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
    5.17      Pos.pos' -> Ctree.ctree -> Calc.T
    5.18  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    5.19 @@ -69,7 +69,7 @@
    5.20  | FormKF of cellID * edit * indent * nest * TermC.as_string                   (*<--*)
    5.21  | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
    5.22  | RefineKF of Stool.match list                                             (*<--*)
    5.23 -| RefinedKF of (Problem.id * ((Model.itm list) * ((bool * term) list)))   (*<--*)
    5.24 +| RefinedKF of (Problem.id * ((I_Model.T) * ((bool * term) list)))   (*<--*)
    5.25  
    5.26  (* 
    5.27    datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
    5.28 @@ -77,7 +77,7 @@
    5.29  datatype mout =
    5.30    FormKF of TermC.as_string
    5.31  | PpcKF of (pblmet * Model.item Model.ppc) 
    5.32 -| RefinedKF of Problem.id * (Model.itm list * (bool * term) list)
    5.33 +| RefinedKF of Problem.id * (I_Model.T * (bool * term) list)
    5.34  | Error' of string
    5.35  | EmptyMout
    5.36  

     6.1 --- a/src/Tools/isac/Specify/i-model.sml	Mon May 04 16:47:32 2020 +0200
     6.2 +++ b/src/Tools/isac/Specify/i-model.sml	Mon May 04 17:08:32 2020 +0200
     6.3 @@ -14,6 +14,9 @@
     6.4    val e_itm : itm 
     6.5  (*\------- to I_Model from Model -------/*)
     6.6  
     6.7 +  type T
     6.8 +  type single
     6.9 +
    6.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    6.11  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    6.12    (* NONE *)
    6.13 @@ -45,5 +48,7 @@
    6.14  val e_itm = (0, [], false, "e_itm", Syn "e_itm");
    6.15  (*\------- to I_Model from Model -------/*)
    6.16  
    6.17 +type T = Model_Def.itm list;
    6.18 +type single = Model_Def.itm;
    6.19  
    6.20  (**)end(**);
    6.21 \ No newline at end of file

     7.1 --- a/src/Tools/isac/Specify/mstools.sml	Mon May 04 16:47:32 2020 +0200
     7.2 +++ b/src/Tools/isac/Specify/mstools.sml	Mon May 04 17:08:32 2020 +0200
     7.3 @@ -9,10 +9,10 @@
     7.4  
     7.5  signature SPECIFY_TOOL =
     7.6  sig
     7.7 -  val check_preconds : 'a -> Rule_Set.T -> term list -> Model.itm list -> (bool * term) list
     7.8 -  val check_preconds' : Rule_Set.T -> term list -> Model.itm list -> 'a -> (bool * term) list
     7.9 +  val check_preconds : 'a -> Rule_Set.T -> term list -> I_Model.T -> (bool * term) list
    7.10 +  val check_preconds' : Rule_Set.T -> term list -> I_Model.T -> 'a -> (bool * term) list
    7.11  
    7.12 -  datatype match_ = Match_ of Problem.id * (Model.itm list * (bool * term) list) | NoMatch_
    7.13 +  datatype match_ = Match_ of Problem.id * (I_Model.T * (bool * term) list) | NoMatch_
    7.14    val refined_ : match_ list -> match_ option
    7.15    datatype match = Matches of Problem.id * Model.item Model.ppc | NoMatch of Problem.id * Model.item Model.ppc
    7.16    val matchs2str : match list -> string
    7.17 @@ -43,7 +43,7 @@
    7.18  
    7.19  (* 10.03 for Refine_Problem *)
    7.20  datatype match_ = 
    7.21 -  Match_ of Problem.id * (( Model.itm list) * ((bool * term) list))
    7.22 +  Match_ of Problem.id * (( I_Model.T) * ((bool * term) list))
    7.23  | NoMatch_;
    7.24  
    7.25  (* the refined pbt is the last_element Matches in the list *)

     8.1 --- a/src/Tools/isac/Specify/o-model.sml	Mon May 04 16:47:32 2020 +0200
     8.2 +++ b/src/Tools/isac/Specify/o-model.sml	Mon May 04 17:08:32 2020 +0200
     8.3 @@ -14,6 +14,9 @@
     8.4    val e_ori: ori
     8.5  (*\------- to O_Model from Model -------/*)
     8.6  
     8.7 +  type T
     8.8 +  type single
     8.9 +
    8.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    8.11  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    8.12    (* NONE *)
    8.13 @@ -34,5 +37,7 @@
    8.14  val oris2str = Model_Def.oris2str;
    8.15  (*\------- to O_Model from Model -------/*)
    8.16  
    8.17 +type T = Model_Def.ori list;
    8.18 +type single = Model_Def.ori
    8.19  
    8.20  (**)end(**);
    8.21 \ No newline at end of file

     9.1 --- a/src/Tools/isac/Specify/ptyps.sml	Mon May 04 16:47:32 2020 +0200
     9.2 +++ b/src/Tools/isac/Specify/ptyps.sml	Mon May 04 17:08:32 2020 +0200
     9.3 @@ -5,25 +5,25 @@
     9.4  
     9.5  signature MODEL_SPECIFY =
     9.6  sig
     9.7 -  val hack_until_review_Specify_1: Method.id -> Model.itm list -> Model.itm list
     9.8 -  val hack_until_review_Specify_2: Method.id -> Model.itm list -> Model.itm list
     9.9 +  val hack_until_review_Specify_1: Method.id -> I_Model.T -> I_Model.T
    9.10 +  val hack_until_review_Specify_2: Method.id -> I_Model.T -> I_Model.T
    9.11    
    9.12    val get_fun_ids : theory -> (string * typ) list
    9.13    type field
    9.14    (* for calchead.sml, if below at left margin *)
    9.15 -  val prep_ori : Celem.fmz_ -> theory -> field list -> Model.ori list * Proof.context
    9.16 +  val prep_ori : Celem.fmz_ -> theory -> field list -> O_Model.T * Proof.context
    9.17    val add_id : 'a list -> (int * 'a) list
    9.18 -  val add_field' : theory -> field list -> Model.ori list -> Model.ori list
    9.19 -  val match_itms_oris : theory -> Model.itm list -> field list * term list * Rule_Set.T ->
    9.20 -    Model.ori list -> bool * (Model.itm list * (bool * term) list)
    9.21 -  val refine_ori : Model.ori list -> Problem.id -> Problem.id option
    9.22 -  val refine_ori' : Model.ori list -> Problem.id -> Problem.id
    9.23 -  val refine_pbl : theory -> Problem.id -> Model.itm list ->
    9.24 -    (Problem.id * (Model.itm list * (bool * term) list)) option
    9.25 +  val add_field' : theory -> field list -> O_Model.T -> O_Model.T
    9.26 +  val match_itms_oris : theory -> I_Model.T -> field list * term list * Rule_Set.T ->
    9.27 +    O_Model.T -> bool * (I_Model.T * (bool * term) list)
    9.28 +  val refine_ori : O_Model.T -> Problem.id -> Problem.id option
    9.29 +  val refine_ori' : O_Model.T -> Problem.id -> Problem.id
    9.30 +  val refine_pbl : theory -> Problem.id -> I_Model.T ->
    9.31 +    (Problem.id * (I_Model.T * (bool * term) list)) option
    9.32  
    9.33    val appc : ('a list -> 'b list) -> 'a Model.ppc -> 'b Model.ppc
    9.34    val mappc : ('a -> 'b) -> 'a Model.ppc -> 'b Model.ppc
    9.35 -  val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc   (* for generate.sml *)
    9.36 +  val itms2itemppc : theory -> I_Model.T -> (bool * term) list -> Model.item Model.ppc   (* for generate.sml *)
    9.37  
    9.38    val get_pbt : Problem.id -> Problem.T
    9.39    val get_met : Method.id -> Method.T                                    (* for generate.sml *)
    9.40 @@ -78,7 +78,7 @@
    9.41  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    9.42    val e_fillpat : string * term * string
    9.43    val coll_vats : ''a list * ('b * ''a list * 'c * 'd * 'e) -> ''a list
    9.44 -  val filter_vat : Model.ori list -> int -> Model.ori list
    9.45 +  val filter_vat : O_Model.T -> int -> O_Model.T
    9.46    val show_metguhs : unit -> unit
    9.47    val sort_metguhs : unit -> unit
    9.48  end
    9.49 @@ -442,7 +442,7 @@
    9.50  (* transform oris *)
    9.51  
    9.52  fun coll_vats (vats, (_, vs, _, _, _)) = union op = vats vs;
    9.53 -fun filter_vat oris i = filter ((member_swap op = i) o (#2 : Model.ori -> int list)) oris;
    9.54 +fun filter_vat oris i = filter ((member_swap op = i) o (#2 : O_Model.single -> int list)) oris;
    9.55  
    9.56  (** check a problem (ie. itm list) for matching a problemtype **)
    9.57  

    10.1 --- a/src/Tools/isac/TODO.thy	Mon May 04 16:47:32 2020 +0200
    10.2 +++ b/src/Tools/isac/TODO.thy	Mon May 04 17:08:32 2020 +0200
    10.3 @@ -27,6 +27,8 @@
    10.4  (*\------- to  from -------/*)
    10.5    \begin{itemize}
    10.6    \item xxx
    10.7 +  \item push nes identifiers back from O/I_Model to Model_Def
    10.8 +  \item xxx
    10.9    \item rename Tactic.Calculate -> Tactic.Evaluate
   10.10    \item xxx
   10.11    \item xxx