1.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml	Mon Apr 19 19:55:31 2021 +0200
     1.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml	Mon Apr 19 20:12:53 2021 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4  "----------- fun avoid_contradict --------------------------------------------------------------";
     1.5  val preds = [
     1.6  (*0.pre*)TermC.str2term "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
     1.7 -(*1.pre*)TermC.str2term ("\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
     1.8 +(*1.pre*)TermC.str2term ("\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
     1.9  (*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x"),
    1.10  (*0.asm*)TermC.str2term  "x \<noteq> 0",             (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*)
    1.11  (*0.asm*)TermC.str2term  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"
    1.12 @@ -203,7 +203,7 @@
    1.13  
    1.14  (*     *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
    1.15  (*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
    1.16 -(*1.pre*)  "\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
    1.17 +(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
    1.18  (*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
    1.19  (*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x", 
    1.20  (*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
    1.21 @@ -249,7 +249,7 @@
    1.22  
    1.23  (*     *)if eq_set op = (map UnparseC.term (get_assumptions ctxt_parent), [
    1.24  (*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
    1.25 -(*1.pre*)  "\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
    1.26 +(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
    1.27  (*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
    1.28  (*0.asm*)  "x \<noteq> 0", 
    1.29  (*0.asm*)  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"
    1.30 @@ -260,7 +260,7 @@
    1.31    ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent;
    1.32  (*     *)if eq_set op = (map UnparseC.term (get_assumptions ctxt'), [
    1.33  (*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
    1.34 -(*1.pre*)  "\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
    1.35 +(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
    1.36  (*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
    1.37  (*0.asm*)  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
    1.38  (*0.asm*)  "x \<noteq> 0",             (* <----------------------- "x \<noteq> 0" contradiction resoved ---\*)
    1.39 @@ -308,7 +308,7 @@
    1.40  if f2str f = "[x = 6 / 5]" andalso map UnparseC.term (Ctree.get_assumptions pt p) =
    1.41   ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
    1.42    "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
    1.43 -  "\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
    1.44 +  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
    1.45    "x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
    1.46    "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"]
    1.47  then () else error "test CHANGED";

     2.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml	Mon Apr 19 19:55:31 2021 +0200
     2.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml	Mon Apr 19 20:12:53 2021 +0200
     2.3 @@ -261,7 +261,7 @@
     2.4  "----------- fun TermC.matches --------------------------------";
     2.5   (*examples see
     2.6     test/../Knowledge/polyeq.sml:     
     2.7 -   Where=[Correct "TermC.matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
     2.8 +   Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
     2.9   (*test/../Specify/refine.sml:        
    2.10     |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
    2.11    val thy = @{theory "Complex_Main"}; 

     3.1 --- a/test/Tools/isac/BridgeJEdit/parseC.sml	Mon Apr 19 19:55:31 2021 +0200
     3.2 +++ b/test/Tools/isac/BridgeJEdit/parseC.sml	Mon Apr 19 20:12:53 2021 +0200
     3.3 @@ -99,14 +99,14 @@
     3.4  val given_comma = Parse.command_name "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term;
     3.5  val given = Parse.command_name "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term;
     3.6  
     3.7 -case ParseC.TermC.parse given_comma (ParseC.tokenize given_comma_str) of
     3.8 +case ParseC.parse given_comma (ParseC.tokenize given_comma_str) of
     3.9    ((("Given", ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
    3.10      []) => ()
    3.11    (*^^^^--------------------------------- is empty:     parsing OK*)
    3.12  | _ => error "TermC.parse given_comma CHANGED";
    3.13  
    3.14  "----------- Parse.list1 DOES expect <,> between elements";
    3.15 -case ParseC.TermC.parse given (ParseC.tokenize given_str) of
    3.16 +case ParseC.parse given (ParseC.tokenize given_str) of
    3.17    ((("Given", ":"), [_(*"<markup>"*)]),
    3.18      [_(*Token (("Streckenlast q_0", ({}, {})), (String, "Streckenlast q_0"), Slot)*)]) => ()
    3.19    (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is NOT empty: parsing NOT ok*)
    3.20 @@ -142,7 +142,7 @@
    3.21      );
    3.22  
    3.23  val toks = ParseC.tokenize model_str;
    3.24 -case ParseC.TermC.parse ParseC.model toks of
    3.25 +case ParseC.parse ParseC.model toks of
    3.26  (((((((((((((((
    3.27    "Model", (("", ""), "")), ":"),
    3.28      "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
    3.29 @@ -153,7 +153,7 @@
    3.30  
    3.31  "----------- Model before student's input";
    3.32  val toks = ParseC.tokenize model_empty_str;
    3.33 -case ParseC.TermC.parse ParseC.model toks of
    3.34 +case ParseC.parse ParseC.model toks of
    3.35  (((((((((((((((
    3.36    "Model", (("", ""), "")), ":"),
    3.37      "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
    3.38 @@ -164,7 +164,7 @@
    3.39  
    3.40  "----------- Model explicitly referring to RProblem (default), not RMethod";
    3.41  val toks = ParseC.tokenize model_str_opt;
    3.42 -case ParseC.TermC.parse ParseC.model toks of
    3.43 +case ParseC.parse ParseC.model toks of
    3.44  (((((((((((((((
    3.45    "Model", (("(", "RProblem"), ")")), ":"),
    3.46      "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
    3.47 @@ -193,11 +193,11 @@
    3.48      "RMethod: [\"\"]"
    3.49      );
    3.50  
    3.51 -case ParseC.TermC.parse ParseC.references (ParseC.tokenize references_collapsed_str) of
    3.52 +case ParseC.parse ParseC.references (ParseC.tokenize references_collapsed_str) of
    3.53    ((("References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])), [])
    3.54    => () | _ => error "TermC.parse references_collapsed CHANGED";
    3.55  
    3.56 -case ParseC.TermC.parse ParseC.references (ParseC.tokenize references_str) of (((
    3.57 +case ParseC.parse ParseC.references (ParseC.tokenize references_str) of (((
    3.58    "References", ":"),
    3.59       ((((((((
    3.60      "RTheory", ":"), "Biegelinie"),
    3.61 @@ -206,7 +206,7 @@
    3.62     [])
    3.63    => () | _ => error "TermC.parse references CHANGED";
    3.64  
    3.65 -case ParseC.TermC.parse ParseC.references (ParseC.tokenize references_empty_str) of (((
    3.66 +case ParseC.parse ParseC.references (ParseC.tokenize references_empty_str) of (((
    3.67    "References", ":"), ((((((((
    3.68      "RTheory", ":"), ""),
    3.69      "RProblem"), ":"), [""]),
    3.70 @@ -253,7 +253,7 @@
    3.71    => () | _ => error "TermC.parse specification (expanded) changed";
    3.72  
    3.73  "----------- Specification collapsed";
    3.74 -case ParseC.TermC.parse ParseC.specification (ParseC.tokenize specification_collapsed_str) of (((
    3.75 +case ParseC.parse ParseC.specification (ParseC.tokenize specification_collapsed_str) of (((
    3.76    "Specification", ":"),
    3.77  (*model*)((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""),
    3.78  (*refs?*)(((((((("", ""), ""), ""), ""), []), ""), ""), [])))),
    3.79 @@ -290,11 +290,11 @@
    3.80  val toks2' = ParseC.tokenize tactic_Rewrite_Set_Inst_str;
    3.81  val toks3' = ParseC.tokenize tactic_Check_Postcond_str;
    3.82  
    3.83 -ParseC.TermC.parse ParseC.tactic toks1'; (* = (("Tactic", "EXEC IMMEDIATELY: Substitute <markup> <markup>"), [])*)
    3.84 -ParseC.TermC.parse ParseC.tactic toks2'; (* = (("Tactic", "EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"), [])*)
    3.85 -ParseC.TermC.parse ParseC.tactic toks3'; (* = (("Tactic", "EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien"), [])*)
    3.86 +ParseC.parse ParseC.tactic toks1'; (* = (("Tactic", "EXEC IMMEDIATELY: Substitute <markup> <markup>"), [])*)
    3.87 +ParseC.parse ParseC.tactic toks2'; (* = (("Tactic", "EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"), [])*)
    3.88 +ParseC.parse ParseC.tactic toks3'; (* = (("Tactic", "EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien"), [])*)
    3.89  
    3.90 -case ParseC.TermC.parse ParseC.tactic (ParseC.tokenize tactic_Substitute_str) of
    3.91 +case ParseC.parse ParseC.tactic (ParseC.tokenize tactic_Substitute_str) of
    3.92    (("Tactic", _(*"EXEC IMMEDIATELY: Substitute <markup> <markup>"*)), [])
    3.93  => () | _ => error "TermC.parse Tactic Substitute CHANGED";
    3.94  
    3.95 @@ -323,12 +323,12 @@
    3.96  val toks3 = ParseC.tokenize steps_nonrec_str;
    3.97  
    3.98  "----------- simple version";
    3.99 -ParseC.TermC.parse ParseC.steps []; (* = ([], []): (string * (string * string)) list * Token.T list *)
   3.100 -ParseC.TermC.parse ParseC.steps toks1; (* = ([("<markup>", ("", ""))], [])*) 
   3.101 -ParseC.TermC.parse ParseC.steps toks2; (* = ([("<markup>", ("Tactic", "EXEC IMMEDIATELY: Check_Postcond Biegelinien"))], [])*)
   3.102 -ParseC.TermC.parse ParseC.steps toks3;
   3.103 +ParseC.parse ParseC.steps []; (* = ([], []): (string * (string * string)) list * Token.T list *)
   3.104 +ParseC.parse ParseC.steps toks1; (* = ([("<markup>", ("", ""))], [])*) 
   3.105 +ParseC.parse ParseC.steps toks2; (* = ([("<markup>", ("Tactic", "EXEC IMMEDIATELY: Check_Postcond Biegelinien"))], [])*)
   3.106 +ParseC.parse ParseC.steps toks3;
   3.107  
   3.108 -case ParseC.TermC.parse ParseC.steps toks3 of
   3.109 +case ParseC.parse ParseC.steps toks3 of
   3.110    ([(_(*"<markup>"*), ("", "")), 
   3.111      (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Substitute <markup> <markup>"*))),
   3.112      (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"*))),
   3.113 @@ -338,7 +338,7 @@
   3.114  => () | _ => error "TermC.parse steps, simple version, CHANGED";
   3.115  
   3.116  "----------- version preparing subproblems";
   3.117 -case ParseC.TermC.parse ParseC.steps_subpbl toks3 of
   3.118 +case ParseC.parse ParseC.steps_subpbl toks3 of
   3.119     ([_(*"EXEC IMMEDIATELY step_term: <markup> (, )"*),
   3.120      _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Substitute <markup> <markup>)"*),
   3.121      _(*"EXEC IMMEDIATELY step_term: <markup> (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in)"*),
   3.122 @@ -357,7 +357,7 @@
   3.123    );
   3.124  val body_str = specification_str ^ solution_str;
   3.125  
   3.126 -case ParseC.TermC.parse ParseC.body (ParseC.tokenize body_str) of ((((((
   3.127 +case ParseC.parse ParseC.body (ParseC.tokenize body_str) of ((((((
   3.128    "Specification", ":"), (((((((((((((((
   3.129      "Model", (("", ""), "")), ":"),
   3.130        "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
   3.131 @@ -384,7 +384,7 @@
   3.132  "----------- whole Problem";
   3.133  val toks = ParseC.tokenize (problem_headline_str ^ specification_str ^ solution_str);
   3.134  
   3.135 -case ParseC.TermC.parse ParseC.problem toks of (((((((
   3.136 +case ParseC.parse ParseC.problem toks of (((((((
   3.137    "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
   3.138      "Specification", ":"), (((((((((((((((
   3.139        "Model", (("", ""), "")), ":"),
   3.140 @@ -414,7 +414,7 @@
   3.141        "References:" ^   (* <<<----- collapsed *)
   3.142      "Solution:"
   3.143    );
   3.144 -case ParseC.TermC.parse ParseC.problem toks of (((((((
   3.145 +case ParseC.parse ParseC.problem toks of (((((((
   3.146    "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
   3.147      "Specification", ":"), (((((((((((((((
   3.148        "Model", (("", ""), "")), ":"),
   3.149 @@ -431,7 +431,7 @@
   3.150  "----------- Problem-headline only";
   3.151  val toks = ParseC.tokenize problem_headline_str;
   3.152  
   3.153 -case ParseC.TermC.parse ParseC.problem toks of (((((((
   3.154 +case ParseC.parse ParseC.problem toks of (((((((
   3.155    "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
   3.156      "", ""), (((((((((((((((
   3.157        "", (("", ""), "")), ""),
   3.158 @@ -453,7 +453,7 @@
   3.159        references_str ^
   3.160      "Solution:"
   3.161    );
   3.162 -case ParseC.TermC.parse ParseC.problem toks of ( ((((((
   3.163 +case ParseC.parse ParseC.problem toks of ( ((((((
   3.164    "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
   3.165      "Specification", ":"), (((((((((((((((
   3.166        "Model", (("", ""), "")), ":"),
   3.167 @@ -472,7 +472,7 @@
   3.168  => () | _ => error "TermC.parse finish specification CHANGED"
   3.169  
   3.170  "----------- Specification collapsed";
   3.171 -case ParseC.TermC.parse ParseC.problem (ParseC.tokenize problem_headline_str) of (((((((
   3.172 +case ParseC.parse ParseC.problem (ParseC.tokenize problem_headline_str) of (((((((
   3.173    "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
   3.174      (*Specification*)"", ""), (((((((((((((((
   3.175        (*Model*)"", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), ((((((((
   3.176 @@ -485,7 +485,7 @@
   3.177  
   3.178  "----------- Problem with final_result, all collapsed";
   3.179  val toks = ParseC.tokenize (problem_headline_str ^ final_result_str);
   3.180 -case ParseC.TermC.parse ParseC.problem toks of (((((((
   3.181 +case ParseC.parse ParseC.problem toks of (((((((
   3.182    "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), (((((
   3.183      (*Specification*)"", ""), (((((((((((((((
   3.184        (*Model*)"", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), ((((((((
   3.185 @@ -507,7 +507,7 @@
   3.186        references_str ^
   3.187      "Solution:"
   3.188    );
   3.189 -case ParseC.TermC.parse ParseC.problem toks |> fst |> ParseC.read_out_problem of
   3.190 +case ParseC.parse ParseC.problem toks |> fst |> ParseC.read_out_problem of
   3.191    {thy_id = "Biegelinie", pbl_id = ["Biegelinien"],
   3.192     givens = [_(*"<markup>"*), _(*"<markup>"*)], wheres = [_(*"<markup>"*), _(*"<markup>"*)],
   3.193       find = _(*"<markup>"*), relates = [_(*"<markup>"*)],
   3.194 @@ -552,7 +552,7 @@
   3.195    ")");
   3.196  
   3.197  val toks = ParseC.tokenize form_single_str;
   3.198 -case ParseC.TermC.parse form_single toks of (((((((((((
   3.199 +case ParseC.parse form_single toks of (((((((((((
   3.200    "(",
   3.201       ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
   3.202         "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
   3.203 @@ -571,7 +571,7 @@
   3.204  formalise: formalise parser;
   3.205  
   3.206  val toks = ParseC.tokenize ("[" ^ form_single_str ^ "]");
   3.207 -case ParseC.TermC.parse formalise (ParseC.tokenize ("[" ^ form_single_str ^ "]")) of ([((((((((((
   3.208 +case ParseC.parse formalise (ParseC.tokenize ("[" ^ form_single_str ^ "]")) of ([((((((((((
   3.209    "(",
   3.210      ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
   3.211        "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",

     4.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml	Mon Apr 19 19:55:31 2021 +0200
     4.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml	Mon Apr 19 20:12:53 2021 +0200
     4.3 @@ -28,7 +28,7 @@
     4.4  
     4.5  val thy = @{theory "Biegelinie"};
     4.6  val ctxt = ThyC.id_to_ctxt "Biegelinie";
     4.7 -fun TermC.str2term str = (Thm.term_of o the o (TermC.parse thy)) str;
     4.8 +fun str2term str = (Thm.term_of o the o (TermC.parse thy)) str;
     4.9  fun term2s t = UnparseC.term_by_thyID "Biegelinie" t;
    4.10  fun rewrit thm str = fst (the (rewrite_ thy tless_true Rule_Set.empty true thm str));
    4.11  

     5.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Mon Apr 19 19:55:31 2021 +0200
     5.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Mon Apr 19 20:12:53 2021 +0200
     5.3 @@ -314,8 +314,8 @@
     5.4  Operand:   L :: real                 ========== L was already present in equalities ========== *)
     5.5  
     5.6  "===== case 1 =====";
     5.7 -val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
     5.8 -case TermC.matches of 
     5.9 +val matches = Refine.refine fmz ["LINEAR", "system"];
    5.10 +case matches of 
    5.11   [M_Match.Matches (["LINEAR", "system"], _),
    5.12    M_Match.Matches (["2x2", "LINEAR", "system"], _),
    5.13    M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _),
    5.14 @@ -333,8 +333,8 @@
    5.15  "===== case 2 =====";
    5.16  val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]", 
    5.17  	   "solveForVars [c, c_2]", "solution LL"];
    5.18 -val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
    5.19 -case TermC.matches of [_,_,
    5.20 +val matches = Refine.refine fmz ["LINEAR", "system"];
    5.21 +case matches of [_,_,
    5.22  		  M_Match.Matches
    5.23  		    (["triangular", "2x2", "LINEAR", "system"],
    5.24  		      {Find = [Correct "solution LL"],
    5.25 @@ -350,11 +350,11 @@
    5.26  | _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
    5.27  
    5.28  (*WN051014---------------------------------------------------------------- 
    5.29 -  the above 'val TermC.matches = Refine.refine fmz ["LINEAR", "system"]'
    5.30 +  the above 'val matches = Refine.refine fmz ["LINEAR", "system"]'
    5.31    didn't work anymore; we investigated in these steps:*)
    5.32  val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]", 
    5.33  	  "solveForVars [c, c_2]", "solution LL"];
    5.34 -val TermC.matches = Refine.refine fmz ["triangular", "2x2", "LINEAR", "system"];
    5.35 +val matches = Refine.refine fmz ["triangular", "2x2", "LINEAR", "system"];
    5.36  (*... resulted in 
    5.37     False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n    
    5.38            [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)
    5.39 @@ -422,7 +422,7 @@
    5.40  	               \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]", 
    5.41  	   "solveForVars [c, c_2]", "solution LL"];
    5.42  Rewrite.trace_on := false;
    5.43 -val TermC.matches = Refine.refine fmz ["2x2", "LINEAR", "system"];
    5.44 +val matches = Refine.refine fmz ["2x2", "LINEAR", "system"];
    5.45  Rewrite.trace_on:=false;
    5.46  (*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
    5.47  (*brought: 'False "length_ es_ = 2"'*)

     6.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Mon Apr 19 19:55:31 2021 +0200
     6.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Mon Apr 19 20:12:53 2021 +0200
     6.3 @@ -58,9 +58,9 @@
     6.4       (Const ("Prog_Expr.pow", _) $ Free _ $ Free _) $ Free ("x", _) => ()
     6.5    | _ => error "integrate.sml: parsing: Integral x^^^2 D x";
     6.6  
     6.7 -val t = str2t "ff x TermC.is_f_x";
     6.8 +val t = str2t "ff x is_f_x";
     6.9  case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
    6.10 -	| _ => error "integrate.sml: parsing: ff x TermC.is_f_x";
    6.11 +	| _ => error "integrate.sml: parsing: ff x is_f_x";
    6.12  
    6.13  
    6.14  "----------- integrate by rewriting ---------------------";
    6.15 @@ -120,15 +120,15 @@
    6.16  if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
    6.17  else error "integrate.sml: eval_new_c ???";
    6.18  
    6.19 -val t = str2t "TermC.matches (?u + new_c ?v) (x ^^^ 2 / 2)";
    6.20 -val SOME (_,t') = eval_matches "" "Prog_Expr.TermC.matches" t thy; term2s t';
    6.21 -if term2s t' = "TermC.matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
    6.22 -else error "integrate.sml: TermC.matches new_c = False";
    6.23 +val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
    6.24 +val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
    6.25 +if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
    6.26 +else error "integrate.sml: matches new_c = False";
    6.27  
    6.28 -val t = str2t "TermC.matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
    6.29 -val SOME (_,t') = eval_matches "" "Prog_Expr.TermC.matches" t thy; term2s t';
    6.30 -if term2s t'="TermC.matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
    6.31 -then () else error "integrate.sml: TermC.matches new_c = True";
    6.32 +val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
    6.33 +val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
    6.34 +if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
    6.35 +then () else error "integrate.sml: matches new_c = True";
    6.36  
    6.37  val t = str2t "ff x TermC.is_f_x";
    6.38  val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
    6.39 @@ -146,7 +146,7 @@
    6.40       rew_ord = ("termlessI",termlessI), 
    6.41       erls = Rule_Set.Empty, 
    6.42       srls = Rule_Set.Empty, calc = [], errpatts = [],
    6.43 -     rules = [Eval ("Prog_Expr.TermC.matches",eval_matches ""),
    6.44 +     rules = [Eval ("Prog_Expr.matches",eval_matches ""),
    6.45        	Eval ("Integrate.is'_f'_x", 
    6.46        	      eval_is_f_x "is_f_x_"),
    6.47        	Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),

     7.1 --- a/test/Tools/isac/Knowledge/logexp.sml	Mon Apr 19 19:55:31 2021 +0200
     7.2 +++ b/test/Tools/isac/Knowledge/logexp.sml	Mon Apr 19 20:12:53 2021 +0200
     7.3 @@ -31,7 +31,7 @@
     7.4  
     7.5  val t = TermC.str2term "(2 log x)";
     7.6  val t = TermC.str2term "(2 log x) = 3";
     7.7 -val t = TermC.str2term "TermC.matches ((?a log x) = ?b) ((2 log x) = 3)";
     7.8 +val t = TermC.str2term "matches ((?a log x) = ?b) ((2 log x) = 3)";
     7.9  TermC.atomty t;
    7.10  
    7.11  

     8.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Apr 19 19:55:31 2021 +0200
     8.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Apr 19 20:12:53 2021 +0200
     8.3 @@ -113,7 +113,7 @@
     8.4    M_Match.Matches' {Find = [Correct "solutions L"], 
     8.5              With = [], 
     8.6              Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"], 
     8.7 -            Where = [Correct "TermC.matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)", 
     8.8 +            Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)", 
     8.9                       Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"], 
    8.10              Relate = []}
    8.11  then () else error "M_Match.match_pbl [expanded,univariate,equation]";

     9.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Apr 19 19:55:31 2021 +0200
     9.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon Apr 19 20:12:53 2021 +0200
     9.3 @@ -552,7 +552,7 @@
     9.4  "----------- Refine.refine Vereinfache ----------------------------------";
     9.5  val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
     9.6  (*default_print_depth 11;*)
     9.7 -val TermC.matches = Refine.refine fmz ["vereinfachen"];
     9.8 +val matches = Refine.refine fmz ["vereinfachen"];
     9.9  (*default_print_depth 3;*)
    9.10  
    9.11  "----- go into details, if it seems not to work -----";

    10.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Mon Apr 19 19:55:31 2021 +0200
    10.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Mon Apr 19 20:12:53 2021 +0200
    10.3 @@ -148,7 +148,7 @@
    10.4  
    10.5  UnparseC.term bdv = "x";
    10.6  UnparseC.terms asms = (* asms from rewriting are missing : vvv *)
    10.7 -  ("[\"<not> TermC.matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
    10.8 +  ("[\"<not> matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
    10.9     "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\", " ^
   10.10     "\"1 / x = 5 is_ratequation_in x\"]");
   10.11  (*
   10.12 @@ -286,7 +286,7 @@
   10.13  
   10.14  (*     *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
   10.15  (*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
   10.16 -(*1.pre*)  "\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
   10.17 +(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
   10.18  (*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
   10.19  (*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x", 
   10.20  (*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
   10.21 @@ -308,7 +308,7 @@
   10.22  if f2str f = "[x = 6 / 5]" andalso eq_set op = (map UnparseC.term (Ctree.get_assumptions pt p),
   10.23   ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
   10.24    "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
   10.25 -  "\<not> TermC.matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
   10.26 +  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
   10.27    "x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
   10.28    "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"])
   10.29  then () else error "test CHANGED";

    11.1 --- a/test/Tools/isac/MathEngine/step.sml	Mon Apr 19 19:55:31 2021 +0200
    11.2 +++ b/test/Tools/isac/MathEngine/step.sml	Mon Apr 19 20:12:53 2021 +0200
    11.3 @@ -106,26 +106,26 @@
    11.4  --------- ([3], Pbl)--------- Step.do_next \<rightarrow> Add_Given equality (-1 + x = 0)---------------------------------- 
    11.5  ========= ([3], Met)========= Step.by_tactic: Apply_Method ["Test", "solve_linear"] ================================== 
    11.6  Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
    11.7 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)"]) , 
    11.8 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) , 
    11.9  Res .....  NONE) 
   11.10  --------- ([3,1], Frm)--------- Step.do_next \<rightarrow> Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv")---------------------------------- 
   11.11  Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
   11.12 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)"]) , 
   11.13 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) , 
   11.14  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,L,R], Rule_Set.empty, SOME e_e, x = 0 + -1 * -1, ORundef, true, false),
   11.15 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)"]) ) 
   11.16 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) ) 
   11.17  ========= ([3,1], Frm)========= Step.by_tactic: Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv") ================================== 
   11.18  Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, true),
   11.19 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)"]) , 
   11.20 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) , 
   11.21  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,L,R], Rule_Set.empty, SOME e_e, x = 0 + -1 * -1, ORundef, true, true),
   11.22 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)"]) ) 
   11.23 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) ) 
   11.24  --------- ([3,1], Res)--------- Step.do_next \<rightarrow> Rewrite_Set "Test_simplify"---------------------------------- 
   11.25  Frm .....  (NONE, 
   11.26  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, x = 1, ORundef, true, false),
   11.27 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)"]) ) 
   11.28 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) ) 
   11.29  ========= ([3,1], Res)========= Step.by_tactic: Rewrite_Set "Test_simplify" ================================== 
   11.30  Frm .....  (NONE, 
   11.31  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,L,R,L,R,R], Rule_Set.empty, SOME e_e, x = 1, ORundef, true, false),
   11.32 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)"]) ) 
   11.33 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)"]) ) 
   11.34  --------- ([3,2], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["LINEAR", "univariate", "equation", "test"]---------------------------------- 
   11.35  Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
   11.36   (''Test'',
   11.37 @@ -133,7 +133,7 @@
   11.38     ''test''), ORundef, true, true),
   11.39  ... ctxt:    []) , 
   11.40  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
   11.41 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.42 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.43  ========= ([3,2], Res)========= Step.by_tactic: Check_Postcond ["LINEAR", "univariate", "equation", "test"] ================================== 
   11.44  Frm ..... (SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, Subproblem
   11.45   (''Test'',
   11.46 @@ -141,31 +141,31 @@
   11.47     ''test''), ORundef, true, true),
   11.48  ... ctxt:    []) , 
   11.49  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x)], [R,R,D,L,R], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
   11.50 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.51 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.52  --------- ([3], Res)--------- Step.do_next \<rightarrow> Check_elementwise "Assumptions"---------------------------------- 
   11.53  Frm .....  (NONE, 
   11.54  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, false),
   11.55 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.56 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.57  ========= ([3], Res)========= Step.by_tactic: Check_elementwise "Assumptions" ================================== 
   11.58  Frm .....  (NONE, 
   11.59  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
   11.60 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.61 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.62  --------- ([4], Res)--------- Step.do_next \<rightarrow> Check_Postcond ["sqroot-test", "univariate", "equation", "test"]---------------------------------- 
   11.63  Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
   11.64  ... ctxt:    []) , 
   11.65  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
   11.66 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.67 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.68  ========= ([4], Res)========= Step.by_tactic: Check_Postcond ["sqroot-test", "univariate", "equation", "test"] ================================== 
   11.69  Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
   11.70  ... ctxt:    []) , 
   11.71  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
   11.72 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.73 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.74  --------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'---------------------------------- 
   11.75  ========= ([], Res)========= Step.by_tactic: input End_Proof' ================================== 
   11.76  Frm ..... (SOME (Pstate ([], [], Rule_Set.empty, NONE, ??.empty, ORundef, false, false),
   11.77  ... ctxt:    []) , 
   11.78  Res .....  SOME (Pstate ([(e_e, -1 + x = 0),(v_v, x),(L_L, [x = 1])], [R,R,D,R,D], Rule_Set.empty, NONE, [x = 1], ORundef, true, true),
   11.79 -... ctxt:    ["TermC.matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.80 +... ctxt:    ["matches (?a = ?b) (-1 + x = 0)", "x = 1"]) ) 
   11.81  --------- ([], Res)--------- Step.do_next \<rightarrow> input End_Proof'---------------------------------- 
   11.82  *)
   11.83  

    12.1 --- a/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml	Mon Apr 19 19:55:31 2021 +0200
    12.2 +++ b/test/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml	Mon Apr 19 20:12:53 2021 +0200
    12.3 @@ -30,7 +30,7 @@
    12.4  (*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
    12.5  
    12.6  ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[]";(*isa*)
    12.7 -((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[\"TermC.matches (?a = ?b) (-1 + x = 0)\"]";(*REP*)
    12.8 +((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[\"matches (?a = ?b) (-1 + x = 0)\"]";(*REP*)
    12.9  (* there are questionable assumptions either ---------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
   12.10  
   12.11  (*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)

    13.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml	Mon Apr 19 19:55:31 2021 +0200
    13.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml	Mon Apr 19 20:12:53 2021 +0200
    13.3 @@ -71,7 +71,7 @@
    13.4    [Problem.prep_input (theory "Isac_Knowledge")
    13.5        (["approximate", "univariate", "equation", "test"],
    13.6          [("#Given", ["equality e_e", "solveFor v_v", "errorBound err_"]),
    13.7 -          ("#Where", ["TermC.matches (?a = ?b) e_e"]),
    13.8 +          ("#Where", ["matches (?a = ?b) e_e"]),
    13.9            ("#Find", ["solutions v_i_"])],
   13.10          Rule_Set.append_rules Rule_Set.empty [Eval ("Prog_Expr.TermC.matches",eval_matches "#matches_")], [])]
   13.11    thy;

    14.1 --- a/test/Tools/isac/Specify/m-match.sml	Mon Apr 19 19:55:31 2021 +0200
    14.2 +++ b/test/Tools/isac/Specify/m-match.sml	Mon Apr 19 20:12:53 2021 +0200
    14.3 @@ -31,7 +31,7 @@
    14.4        Correct "solveFor x",
    14.5        Superfl "errorBound (eps = 0)"],
    14.6      Relate = [],
    14.7 -    Where = [Correct "TermC.matches (?a = ?b) (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"],
    14.8 +    Where = [Correct "matches (?a = ?b) (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"],
    14.9      With = []} => ()
   14.10    | _ => error "M_Match.match_pbl CHANGED";
   14.11  

    15.1 --- a/test/Tools/isac/Specify/refine.sml	Mon Apr 19 19:55:31 2021 +0200
    15.2 +++ b/test/Tools/isac/Specify/refine.sml	Mon Apr 19 20:12:53 2021 +0200
    15.3 @@ -346,7 +346,7 @@
    15.4     Where = [False www(*! ! ! ! ! !*)],
    15.5     Relate = [],...}) => www(*! ! !*)
    15.6  | _ => error "--- Refine_Problem broken 1";
    15.7 -if www = "TermC.matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"
    15.8 +if www = "matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"
    15.9  then () else error "--- Refine_Problem broken 2";
   15.10  (*ML> f; 
   15.11  val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef,
   15.12 @@ -354,7 +354,7 @@
   15.13           {Find=[Incompl "solutions []"],
   15.14            Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
   15.15                   Correct "solveFor x"],Relate=[],
   15.16 -          Where=[False "TermC.matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
   15.17 +          Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
   15.18                  |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
   15.19                  |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)
   15.20          |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
   15.21 @@ -420,10 +420,10 @@
   15.22        (*if*) not preok (*then*);
   15.23  
   15.24  (*+*)Pre_Conds.to_string xxxxx = "[\n" ^
   15.25 -  "(false, TermC.matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\n" ^
   15.26 -    "TermC.matches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\n" ^
   15.27 -    "TermC.matches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\n" ^
   15.28 -    "TermC.matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8))]";
   15.29 +  "(false, matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\n" ^
   15.30 +    "matches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\n" ^
   15.31 +    "matches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\n" ^
   15.32 +    "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8))]";
   15.33    (*TermC.matches  ^^^^^^^^^^^^^^^^ NONE, ok: why then NONE = Refine.problem below?*)
   15.34  (*-------------------- stop step into find_next_step ----------------------------------------*)
   15.35  (*+ continue after find_next_step*)val (p_', tac) = (p_'_'''''_', tac'''''_')

    16.1 --- a/test/Tools/isac/Test_Code/test-code.sml	Mon Apr 19 19:55:31 2021 +0200
    16.2 +++ b/test/Tools/isac/Test_Code/test-code.sml	Mon Apr 19 20:12:53 2021 +0200
    16.3 @@ -47,6 +47,6 @@
    16.4  
    16.5  if p = ([], Res) andalso f2str t = "[x = 1]" andalso
    16.6    eq_set op = (get_ctxt pt p |> get_assumptions |> map UnparseC.term,
    16.7 -    ["precond_rootmet x", "TermC.matches (?a = ?b) (-1 + x = 0)", "x = 1"])
    16.8 +    ["precond_rootmet x", "matches (?a = ?b) (-1 + x = 0)", "x = 1"])
    16.9  then case nxt of End_Proof' => () | _ => error "fun me_trace all Minisubpbl CHANGED 1"
   16.10  else error "fun me_trace all Minisubpbl CHANGED 2";