1.1 --- a/test/Tools/isac/Specify/refine.thy	Fri Dec 09 16:29:04 2022 +0100
     1.2 +++ b/test/Tools/isac/Specify/refine.thy	Thu Dec 15 13:03:51 2022 +0100
     1.3 @@ -12,55 +12,63 @@
     1.4    *setup* Know_Store.add_pbls is impossible in *.sml files.
     1.5    The respective test/../refine.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  \<close> ML \<open>
    1.13  (* cp from problem.sml, Outer_Syntax.command \<^command_keyword>\<open>problem\<close> *)
    1.14    val arg_1 = Problem.prep_store thy "pbl_test_refine" [] Problem.id_empty
    1.15      ([], [], NONE) (["refine", "test"], [], Rule_Set.empty)
    1.16  
    1.17 -  val (model, where_) = Model_Pattern.parse ctxt
    1.18 +  val (model, where_) = Model_Pattern.parse_pos ctxt
    1.19      [("#Given", [("fixedValues a_a", Position.none)])]
    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_pbla" [] Problem.id_empty
    1.22 -    (model, where_, NONE) (["pbla", "refine", "test"], [], Rule_Set.empty)
    1.23 +    (model', where_', NONE) (["pbla", "refine", "test"], [], Rule_Set.empty)
    1.24  
    1.25 -  val (model, where_) = Model_Pattern.parse ctxt
    1.26 -    [("#Given", [("fixedValues a_a", Position.none),
    1.27 -                 ("maximum a_1", Position.none)])]
    1.28 +  val (model, where_) = Model_Pattern.parse_pos ctxt
    1.29 +    [("#Given", [("fixedValues a_a", Position.none), ("maximum a_1", Position.none)])]
    1.30 +  val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
    1.31    val arg_3 = Problem.prep_store thy "pbl_pbla1" [] Problem.id_empty
    1.32 -    (model, where_, NONE) (["pbla1", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.33 +    (model', where_', NONE) (["pbla1", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.34  
    1.35 -  val (model, where_) = Model_Pattern.parse ctxt
    1.36 -    [("#Given", [("fixedValues a_a", Position.none),
    1.37 -                 ("valuesFor a_2", Position.none)])]
    1.38 +  val (model, where_) = Model_Pattern.parse_pos ctxt
    1.39 +    [("#Given", [("fixedValues a_a", Position.none), ("valuesFor a_2", Position.none)])]
    1.40 +  val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
    1.41    val arg_4 = Problem.prep_store thy "pbl_pbla2" [] Problem.id_empty
    1.42 -    (model, where_, NONE) (["pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.43 +    (model', where_', NONE) (["pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.44  
    1.45 -  val (model, where_) = Model_Pattern.parse ctxt
    1.46 +  val (model, where_) = Model_Pattern.parse_pos ctxt
    1.47      [("#Given", [("fixedValues a_a", Position.none),
    1.48                   ("valuesFor a_2", Position.none),
    1.49                   ("functionOf a2_x", Position.none)])]
    1.50 +  val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
    1.51    val arg_5 = Problem.prep_store thy "pbl_pbla2x" [] Problem.id_empty
    1.52 -    (model, where_, NONE) (["pbla2x", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.53 +    (model', where_', NONE) (["pbla2x", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.54  
    1.55 -  val (model, where_) = Model_Pattern.parse ctxt
    1.56 +  val (model, where_) = Model_Pattern.parse_pos ctxt
    1.57      [("#Given", [("fixedValues a_a", Position.none),
    1.58                   ("valuesFor a_2", Position.none),
    1.59                   ("boundVariable a2_y", Position.none)])]
    1.60 +  val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
    1.61    val arg_6 = Problem.prep_store thy "pbl_pbla2y" [] Problem.id_empty
    1.62 -    (model, where_, NONE) (["pbla2y", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.63 +    (model', where_', NONE) (["pbla2y", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.64  
    1.65 -  val (model, where_) = Model_Pattern.parse ctxt
    1.66 +  val (model, where_) = Model_Pattern.parse_pos ctxt
    1.67      [("#Given", [("fixedValues a_a", Position.none),
    1.68                   ("valuesFor a_2", Position.none),
    1.69                   ("interval a2_z", Position.none)])]
    1.70    val arg_7 = Problem.prep_store thy "pbl_pbla2z" [] Problem.id_empty
    1.71 -    (model, where_, NONE) (["pbla2z", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.72 +    (model', where_', NONE) (["pbla2z", "pbla2", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.73  
    1.74 -  val (model, where_) = Model_Pattern.parse ctxt
    1.75 +  val (model, where_) = Model_Pattern.parse_pos ctxt
    1.76      [("#Given", [("fixedValues a_a", Position.none),
    1.77                   ("relations a_3", Position.none)])]
    1.78 +  val (model', where_') = (map drop_pos_model model, map drop_pos_where_ where_)
    1.79    val arg_8 = Problem.prep_store thy "pbl_pbla3" [] Problem.id_empty
    1.80 -    (model, where_, NONE) (["pbla3", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.81 +    (model', where_', NONE) (["pbla3", "pbla", "refine", "test"], [], Rule_Set.empty)
    1.82  \<close>
    1.83  setup \<open>Know_Store.add_pbls @{context} [arg_1, arg_2, arg_3, arg_4, arg_5, arg_6, arg_7, arg_8]\<close>
    1.84