1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml	Mon Jan 30 12:38:17 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml	Tue Jan 31 10:49:17 2023 +0100
     1.3 @@ -372,7 +372,7 @@
     1.4  val ctxt = Proof_Context.init_global thy;
     1.5  
     1.6  (*---------- (1) with Free A, B  ----------------------------------------------------------------*)
     1.7 -val t = (the o (parseNEW  ctxt)) "3 = A / 2 + A / 4 + (B / 2 + - 1 * B / (2::real))";
     1.8 +val t = (the o (ParseC.term_opt  ctxt)) "3 = A / 2 + A / 4 + (B / 2 + - 1 * B / (2::real))";
     1.9                                  (* required for applying thms in rewriting  \<up> ^*)
    1.10  (* we get details from here..*)
    1.11  
    1.12 @@ -381,7 +381,7 @@
    1.13  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
    1.14                       (* |||||||||||||||||||||||||||||||||||| *)
    1.15  
    1.16 -val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)
    1.17 +val t = (the o (ParseC.term_opt  ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)
    1.18                         "A / 2 + A / 4 + (B / 2 + - 1 * B / (2::real))";
    1.19  "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
    1.20  val NONE = (*case*) check_frac_sum t (*of*)
    1.21 @@ -389,7 +389,7 @@
    1.22  (* Rewrite.trace_on:
    1.23  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
    1.24                       (*         |||||||||||||||||||||||||||| *)
    1.25 -val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
    1.26 +val t = (the o (ParseC.term_opt  ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
    1.27                                 "A / 4 + (B / 2 + - 1 * B / (2::real))";
    1.28  "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
    1.29  val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
    1.30 @@ -413,7 +413,7 @@
    1.31  | _ => error "monom_of_term Free changed 2";
    1.32  
    1.33  (*---------- (2) with Const AA, BB --------------------------------------------------------------*)
    1.34 -val t = (the o (parseNEW  ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + - 1 * BB / 2)";
    1.35 +val t = (the o (ParseC.term_opt  ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + - 1 * BB / 2)";
    1.36                                      (*AA :: real*)
    1.37  (* we get details from here..*)
    1.38  
    1.39 @@ -421,7 +421,7 @@
    1.40  (* Rewrite.trace_on:
    1.41  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
    1.42                       (* |||||||||||||||||||||||||||||||||||| *)
    1.43 -val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| *)
    1.44 +val t = (the o (ParseC.term_opt  ctxt))(* ||||||||||||||||||||||||| *)
    1.45                     "AA / 2 + AA / 4 + (BB / 2 + - 1 * BB / 2)";
    1.46  "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
    1.47  val NONE = (*case*) check_frac_sum t (*of*)
    1.48 @@ -750,7 +750,7 @@
    1.49  if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
    1.50     andalso ThmC.string_of_thm thm = 
    1.51             (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
    1.52 -               (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \<up> 2"))) then ()
    1.53 +               (Trueprop $ (ParseC.parse_test ctxt "9 = 3 \<up> 2"))) then ()
    1.54  else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
    1.55  \---------------------------------------------------------------------------------------/*)
    1.56  
    1.57 @@ -769,7 +769,7 @@
    1.58    val SOME (r as (Thm (str, thm))) = nex revsets t;
    1.59  if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
    1.60     ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
    1.61 -                (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \<up> 2"))) then ()
    1.62 +                (Trueprop $ (ParseC.parse_test ctxt "9 = 3 \<up> 2"))) then ()
    1.63  else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
    1.64  
    1.65  (*check the next rule*)
    1.66 @@ -1601,7 +1601,7 @@
    1.67  "-------- fun eval_get_denominator -------------------------------------------";
    1.68  val thy = @{theory Isac_Knowledge};
    1.69  val ctxt = Proof_Context.init_global thy;
    1.70 -val t = TermC.parseNEW' ctxt "get_denominator ((a +x)/b)";
    1.71 +val t = ParseC.parse_test ctxt "get_denominator ((a +x)/b)";
    1.72  val SOME (_, t') = eval_get_denominator "" 0 t ctxt;
    1.73  if UnparseC.term t' = "get_denominator ((a + x) / b) = b"
    1.74  then () else error "get_denominator ((a + x) / b) = b"