1.1 --- a/test/Tools/isac/ProgLang/calculate.thy	Fri Dec 09 16:29:04 2022 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/calculate.thy	Thu Dec 15 13:03:51 2022 +0100
     1.3 @@ -11,6 +11,10 @@
     1.4    *setup* Know_Store.add_pbls / add_mets is impossible in *.sml files.
     1.5    The respective test/../evaluate.sml is called in Test_Isac.thy.
     1.6  \<close> ML \<open>
     1.7 +(*/----- local in struct Problem -------------\*)
     1.8 +val drop_pos_model = (fn (a, b, _) => (a, b))
     1.9 +val drop_pos_where_ = (fn (b, _) => b)
    1.10 +(*\----- local in struct Problem -------------/*)
    1.11  val thy = @{theory "Test"}
    1.12              val arg_1 = Problem.prep_store thy "pbl_ttest" [] Problem.id_empty
    1.13                ([], [], NONE) (["test"], [], Rule_Set.empty)
    1.14 @@ -19,9 +23,10 @@
    1.15                     ("#Find", [("realTestFind s_s", Position.none)])]
    1.16  (* cp from problem.sml, Outer_Syntax.command \<^command_keyword>\<open>problem\<close> *)
    1.17              val ctxt = Proof_Context.init_global thy
    1.18 -            val (model, where_) = Model_Pattern.parse ctxt model_input
    1.19 +            val (model, where_) = Model_Pattern.parse_pos ctxt model_input
    1.20 +            val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
    1.21              val arg_2 = Problem.prep_store thy "pbl_ttest_calc" [] Problem.id_empty
    1.22 -              (model, where_, NONE)
    1.23 +              (model', where_', NONE)
    1.24                (["calculate", "test"], [["Test", "test_calculate"]], Rule_Set.empty)
    1.25  \<close> 
    1.26  setup \<open>Know_Store.add_pbls @{context} [arg_1, arg_2]\<close>
    1.27 @@ -39,7 +44,8 @@
    1.28  val model_input = [("#Given", [("realTestGiven t_t", Position.none)]),
    1.29                     ("#Find", [("realTestFind s_s", Position.none)])]
    1.30  (* cp from method.sml, Outer_Syntax.command \<^command_keyword>\<open>method\<close> *)
    1.31 -          val (model, where_) = Model_Pattern.parse ctxt model_input
    1.32 +          val (model, where_) = Model_Pattern.parse_pos ctxt model_input
    1.33 +          val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
    1.34            val ml_input =
    1.35              {rew_ord = "sqrt_right", rls'= tval_rls, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty,
    1.36              calc = [("PLUS", (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
    1.37 @@ -49,7 +55,7 @@
    1.38              errpats = [], rew_rls = Rule_Set.empty} : MethodC.ml_input
    1.39            val thm = @{thm calc_test.simps}
    1.40            val arg = MethodC.prep_store thy "met_testcal" [] Problem.id_empty
    1.41 -            (["Test", "test_calculate"], model, where_, ml_input, thm)
    1.42 +            (["Test", "test_calculate"], model', where_', ml_input, thm)
    1.43  \<close> 
    1.44  setup \<open>Know_Store.add_mets @{context} [arg]
    1.45  \<close>