1.1 --- a/src/Tools/isac/Specify/m-match.sml	Wed Nov 09 15:15:24 2022 +0100
     1.2 +++ b/src/Tools/isac/Specify/m-match.sml	Thu Nov 10 14:25:38 2022 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    val matchs2str : T list -> string
     1.5  (*/------- rename: TODO 220917 review -------\*)
     1.6  (*val o_model: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool*)
     1.7 -  val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool
     1.8 +  val match_oris: Proof.context -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool
     1.9  (*unify                     ^^^^^^^^^^                                  vvvvvvvvvv 
    1.10                               vvvvvvvvv    ^^^^^^^^^*)
    1.11  (*val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
    1.12 @@ -63,7 +63,7 @@
    1.13  
    1.14  (* check an ori for matching a problemtype by description; 
    1.15     returns true only for itms found in pbt              *)
    1.16 -fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
    1.17 +fun chk1_ pbt (i, vats, f, d, vs) =
    1.18    case find_first (eq1 d) pbt of 
    1.19  	  SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))]
    1.20    | NONE => [];
    1.21 @@ -81,23 +81,23 @@
    1.22    
    1.23  (* check a problem (ie. ori list) for matching a problemtype, 
    1.24     takes the I_Model.variables for concluding completeness (FIXME could be another!) *)
    1.25 -fun match_oris thy where_rls oris (pbt,where_) = 
    1.26 +fun match_oris ctxt where_rls oris (pbt,where_) = 
    1.27    let
    1.28 -    val itms = (flat o (map (chk1_ thy pbt))) oris;
    1.29 +    val itms = (flat o (map (chk1_ pbt))) oris;
    1.30      val mvat = I_Model.variables itms;
    1.31      val complete = chk1_mis mvat itms pbt;
    1.32 -    val (pb, _(*where_'*)) = Pre_Conds.check where_rls where_ itms mvat;
    1.33 +    val (pb, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_ itms mvat;
    1.34    in if complete andalso pb then true else false end;
    1.35  
    1.36  (* check a problem (ie. ori list) for matching a problemtype, 
    1.37     returns items for output to math-experts *)
    1.38  fun match_oris' thy oris (model, where_, where_rls) =
    1.39    let
    1.40 -    val itms = (flat o (map (chk1_ thy model))) oris;
    1.41 +    val itms = (flat o (map (chk1_ model))) oris;
    1.42      val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
    1.43      val mvat = I_Model.variables itms;
    1.44      val miss = chk1_mis' oris model;
    1.45 -    val (pb, where_')  = Pre_Conds.check where_rls where_ itms mvat;
    1.46 +    val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms mvat;
    1.47    in (miss = [] andalso pb, (itms @ miss @ sups, where_')) end;
    1.48  
    1.49  
    1.50 @@ -112,7 +112,7 @@
    1.51              (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
    1.52              (3) newitms = filter (mv mem vat(news)) news 
    1.53     (4) pbt @ newitms                                           *)
    1.54 -fun match_itms_oris (_: theory) pbl (pbt, where_, where_rls) oris =
    1.55 +fun match_itms_oris ctxt pbl (pbt, where_, where_rls) oris =
    1.56    let 
    1.57   (*0*)val mv = I_Model.max_variant pbl;
    1.58  
    1.59 @@ -128,7 +128,7 @@
    1.60   (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
    1.61        val newitms = filter mem_vat news;
    1.62   (*4*)val itms' = pbl @ newitms;
    1.63 -      val (pb, where_') = Pre_Conds.check where_rls where_ itms' mv;
    1.64 +      val (pb, where_') = Pre_Conds.check ctxt where_rls where_ itms' mv;
    1.65    in (length mis = 0 andalso pb, (itms', where_')) end;
    1.66  
    1.67