1.1 --- a/src/Tools/isac/Specify/m-match.sml	Sun Aug 27 17:56:50 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/m-match.sml	Tue Aug 29 08:35:46 2023 +0200
     1.3 @@ -85,15 +85,6 @@
     1.4    
     1.5  (* check a problem (ie. ori list) for matching a problemtype, 
     1.6     takes the I_Model.variables for concluding completeness (FIXME could be another!) *)
     1.7 -(*T_TESTold* )
     1.8 -fun match_oris ctxt where_rls oris (pbt, where_) = 
     1.9 -  let
    1.10 -    val itms = (flat o (map (chk1_ pbt))) oris;
    1.11 -    val mvat = I_Model.variables itms;
    1.12 -    val complete = chk1_mis mvat itms pbt;
    1.13 -    val (pb, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_ itms mvat;
    1.14 -  in if complete andalso pb then true else false end;
    1.15 -( *T_TEST**)
    1.16  fun match_oris ctxt where_rls o_model (model_pattern, where_) = 
    1.17    let
    1.18      val i_model = (flat o (map (chk1_ model_pattern))) o_model;
    1.19 @@ -102,20 +93,9 @@
    1.20      val (pb, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_
    1.21        (model_pattern, I_Model.OLD_to_TEST i_model);
    1.22    in if complete andalso pb then true else false end;
    1.23 -(*T_TESTnew*)
    1.24  
    1.25  (* check a problem (ie. ori list) for matching a problemtype, 
    1.26     returns items for output to math-experts *)
    1.27 -(*T_TESTold* )
    1.28 -fun match_oris' thy oris (model, where_, where_rls) =
    1.29 -  let
    1.30 -    val itms = (flat o (map (chk1_ model))) oris;
    1.31 -    val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
    1.32 -    val mvat = I_Model.variables itms;
    1.33 -    val miss = chk1_mis' oris model;
    1.34 -    val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms mvat;
    1.35 -  in (miss = [] andalso pb, (itms @ miss @ sups, where_')) end;
    1.36 -( *T_TEST**)
    1.37  fun match_oris' thy o_model (model, where_, where_rls) =
    1.38    let
    1.39      val i_model = (flat o (map (chk1_ model))) o_model;
    1.40 @@ -124,7 +104,6 @@
    1.41      val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ 
    1.42        (model, I_Model.OLD_to_TEST i_model);
    1.43    in (miss = [] andalso pb, (i_model @ miss @ sups, where_')) end;
    1.44 -(*T_TESTnew*)
    1.45  
    1.46  
    1.47  (** check a problem (ie. itm list) for matching a problemtype **)
    1.48 @@ -138,26 +117,6 @@
    1.49              (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
    1.50              (3) newitms = filter (mv mem vat(news)) news 
    1.51     (4) pbt @ newitms                                           *)
    1.52 -(*T_TESTold* )
    1.53 -fun match_itms_oris ctxt pbl (pbt, where_, where_rls) oris =
    1.54 -  let 
    1.55 - (*0*)val mv = Pre_Conds.max_variant pbl;
    1.56 -
    1.57 -      fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
    1.58 -      fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
    1.59 -				SOME _ => false | NONE => true;
    1.60 - (*1*)val mis = (filter (notmem pbl)) pbt;
    1.61 -
    1.62 -      fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
    1.63 -      fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
    1.64 - (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
    1.65 -      val news = (flat o (map (oris2itms oris))) mis;
    1.66 - (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
    1.67 -      val newitms = filter mem_vat news;
    1.68 - (*4*)val itms' = pbl @ newitms;
    1.69 -      val (pb, where_') = Pre_Conds.check ctxt where_rls where_ itms' mv;
    1.70 -  in (length mis = 0 andalso pb, (itms', where_')) end;
    1.71 -( *T_TEST**)
    1.72  fun match_itms_oris ctxt pbl (pbt, where_, where_rls) oris =
    1.73    let 
    1.74   (*0*)val mv = Pre_Conds.max_variant pbl;
    1.75 @@ -177,7 +136,6 @@
    1.76        val (pb, where_') = Pre_Conds.check ctxt where_rls where_ 
    1.77          (pbt, I_Model.OLD_to_TEST itms');
    1.78    in (length mis = 0 andalso pb, (itms', where_')) end;
    1.79 -(*T_TESTnew*)
    1.80  
    1.81  
    1.82  (** for use by math-authors **)