1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Tue Oct 03 16:33:54 2023 +0200
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Wed Oct 25 12:34:12 2023 +0200
     1.3 @@ -303,6 +303,13 @@
     1.4    | [a] => (f, a)
     1.5    | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
     1.6  
     1.7 +(*
     1.8 +  The sequence of \<open>formals\<close> and \<open>actuals\<close> must be the same:
     1.9 +  the sequence of \<open>formals\<close> is given by the program,
    1.10 +  the sequence of \<open>actuals\<close> is given by the by theMethodC#model
    1.11 +
    1.12 +  In case of equal sequence the \<open>fun relate\<close> could be simpler ...
    1.13 +*)
    1.14  fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
    1.15      raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
    1.16    | relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
    1.17 @@ -321,14 +328,11 @@
    1.18    let
    1.19      val (model_patt, program, prog, prog_rls, where_, where_rls) =
    1.20        case MethodC.from_store ctxt met_id of
    1.21 -        {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
    1.22 +        {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
    1.23            (model_patt, program, prog, prog_rls, where_, where_rls)
    1.24        | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
    1.25 -(*OLD* )
    1.26 -    val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
    1.27 -( *---*)
    1.28      val (env_model, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model;
    1.29 -(*NEW*)
    1.30 +
    1.31      val actuals = map snd env_model
    1.32      val formals = Program.formal_args prog    
    1.33      val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))