1.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml	Tue May 05 13:33:23 2020 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml	Tue May 05 15:39:20 2020 +0200
     1.3 @@ -41,14 +41,14 @@
     1.4  (*    val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
     1.5  			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
     1.6  ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*)
     1.7 -"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : ori list), ((dI', pI', mI') : Spec.T),
     1.8 -  ((pbl : itm list), (met : itm list)), (pbt, mpc), ((dI, pI, mI) : Spec.T)) = 
     1.9 +"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : O_Model.T), ((dI', pI', mI') : Spec.T),
    1.10 +  ((pbl : I_Model.T), (met : I_Model.T)), (pbt, mpc), ((dI, pI, mI) : Spec.T)) = 
    1.11    (p_, pb, oris, (dI',pI',mI'), (probl, meth), 
    1.12  			    (ppc, (#ppc o get_met) cmI), (dI, pI, mI));
    1.13  
    1.14  dI' = ThyC.id_empty andalso dI = ThyC.id_empty; (* = false*)
    1.15  pI' = Problem.id_empty andalso pI = Problem.id_empty; (* = false*)
    1.16 -find_first (is_error o #5) (pbl:itm list); (* = NONE*)
    1.17 +find_first (is_error o #5) (pbl:I_Model.T); (* = NONE*)
    1.18  
    1.19  (* nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl; 
    1.20  = SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *)
    1.21 @@ -58,13 +58,13 @@
    1.22  fun x mem [] = false
    1.23    | x mem (y :: ys) = x = y orelse x mem ys;
    1.24  in 
    1.25 -    fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
    1.26 +    fun testr_vt v ori = (curry (op mem) v) (#2 (ori:O_Model.single))
    1.27        andalso (#3 ori) <>"#undef";
    1.28 -    fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
    1.29 -    fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
    1.30 -    fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = 
    1.31 +    fun testi_vt v itm = (curry (op mem) v) (#2 (itm:I_Model.single));
    1.32 +    fun test_id ids r = curry (op mem) (#1 (r:O_Model.single)) ids;
    1.33 +    fun test_subset (itm:I_Model.single) ((_,_,_,d,ts):O_Model.single) = 
    1.34  	(d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
    1.35 -    fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
    1.36 +    fun false_and_not_Sup((i,v,false,f,Sup _):I_Model.single) = false
    1.37        | false_and_not_Sup (i,v,false,f, _) = true
    1.38        | false_and_not_Sup  _ = false;
    1.39  end
    1.40 @@ -78,7 +78,7 @@
    1.41  
    1.42  (* SOME (geti_ct thy ori (hd icl))
    1.43  ERROR: SOME (geti_ct thy ori (hd icl))*)
    1.44 -"~~~~~ fun geti_ct, args:"; val (thy, ((_, _, _, d, ts) : ori), ((_, _, _, fd, itm_) : itm)) =
    1.45 +"~~~~~ fun geti_ct, args:"; val (thy, ((_, _, _, d, ts) : O_Model.single), ((_, _, _, fd, itm_) : I_Model.single)) =
    1.46    (thy, ori, (hd icl));
    1.47  "~~~~~ to  return val:"; val xxx = 
    1.48    ( fd,