1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sun Dec 10 07:56:02 2023 +0100
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Sun Dec 10 17:35:07 2023 +0100
     1.3 @@ -27,11 +27,9 @@
     1.4    val tac_from_prog: Ctree.state -> term -> Tactic.input
     1.5  
     1.6  (*from isac_test for Minisubpbl*)
     1.7 -  val arguments_from_model : Proof.context -> MethodC.id -> I_Model.T -> term list
     1.8 +  val arguments_from_model: Proof.context -> MethodC.id -> I_Model.T_POS -> term list
     1.9    val errmsg: string
    1.10 -  val error_msg_2: Proof.context -> term -> I_Model.T -> string
    1.11 -  val error_msg_2_POS: Proof.context -> term -> I_Model.T_POS -> string
    1.12 -  val error_msg_1: string
    1.13 +  val error_msg: string
    1.14    val relate_args: Env.T -> term list -> term list -> Proof.context -> Program.term ->
    1.15      MethodC.id -> term list -> term list -> (term * term) list
    1.16  
    1.17 @@ -57,24 +55,19 @@
    1.18      Option.map (subst_atomic env) (Prog_Tac.get_first_argument prog)
    1.19    | implicit_take _ _ _ = raise ERROR "implicit_take: no match";
    1.20  
    1.21 -val error_msg_1 = "ERROR: the guard is missing (#model in 'type met' added in prep_met)."
    1.22 -fun error_msg_2 ctxt d itms =
    1.23 -  ("arguments_from_model: '" ^ UnparseC.term ctxt d ^ "' not in itms:\n" ^
    1.24 -  "itms:\n" ^ I_Model.to_string @{context} itms)
    1.25 -fun error_msg_2_POS ctxt d itms =
    1.26 -  ("arguments_from_model: '" ^ UnparseC.term ctxt d ^ "' not in itms:\n" ^
    1.27 -  "itms:\n" ^ I_Model.to_string_POS @{context} itms)
    1.28 +val error_msg = "ERROR: the guard is missing (#model in 'type met' added in prep_met)."
    1.29  (* turn Model-items into arguments for a program *)
    1.30 -fun arguments_from_model ctxt mI itms =
    1.31 +fun arguments_from_model ctxt met_id i_model =
    1.32    let
    1.33 -    val mvat = Pre_Conds.max_variant itms
    1.34 -    fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
    1.35 -    val itms = filter (okv mvat) itms
    1.36 -    fun itm2arg _ (_, (_, _)) = [](*this limits errors to init_pstate,
    1.37 -      while changing I_Model.penvval_in triggers much more errors*)
    1.38 -    val pats = (#model o MethodC.from_store ctxt) mI
    1.39 -    val _ = if pats = [] then raise ERROR error_msg_1 else ()
    1.40 -  in (flat o (map (itm2arg itms))) pats end;
    1.41 +    val {model = met_patt, ...} = MethodC.from_store ctxt met_id
    1.42 +    val max_vnt = Model_Def.max_variants'' i_model |> last_elem
    1.43 +  in
    1.44 +    i_model
    1.45 +      |> filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts)
    1.46 +      |> I_Model.order_by_patt met_patt
    1.47 +      |> I_Model.get_values
    1.48 +      |> map Model_Def.values_to_present
    1.49 +  end
    1.50  
    1.51  (*
    1.52    convert a Prog_Tac to Tactic.input;