1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  val ctxt = Proof_Context.init_global @{theory}
     1.5  val prog_expr = get_rls @{context} "prog_expr"
     1.6  
     1.7 -val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
     1.8 +val t = TermC.parse_test @{context} "NTH 1 [a,b,c,d,e]";
     1.9  TermC.atomty t;
    1.10  val thm = Thm.prop_of @{thm NTH_NIL};
    1.11  TermC.atomty thm;
    1.12 @@ -55,8 +55,8 @@
    1.13  if UnparseC.term t' = "a" then () 
    1.14  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.15  
    1.16 -val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
    1.17 -case TermC.str2term "NTH 3 [a,b,c,d,e]" of
    1.18 +val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
    1.19 +case TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]" of
    1.20   Const (\<^const_name>\<open>NTH\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
    1.21       (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
    1.22         (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $
    1.23 @@ -71,7 +71,7 @@
    1.24  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.25  
    1.26  (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    1.27 -val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
    1.28 +val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]";
    1.29  TermC.atomty t;
    1.30  
    1.31  val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;
    1.32 @@ -84,7 +84,7 @@
    1.33  val prog_expr = get_rls @{context} "prog_expr"
    1.34  
    1.35  val thy = @{theory ListC};
    1.36 -val t = TermC.str2term "Length [1, 1, 1]";
    1.37 +val t = TermC.parse_test @{context} "Length [1, 1, 1]";
    1.38  val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.39  UnparseC.term t = "1 + Length [1, 1]";
    1.40  val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.41 @@ -97,12 +97,12 @@
    1.42  if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
    1.43  else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
    1.44  
    1.45 -val t = TermC.str2term "Length [1, 1, 1]";
    1.46 +val t = TermC.parse_test @{context} "Length [1, 1, 1]";
    1.47  val SOME (t, asm) = rewrite_set_ ctxt false prog_expr t;
    1.48  if UnparseC.term t = "3" then ()
    1.49  else error "Length [1, 1, 1] = 3  ..prog_expr changed";
    1.50  
    1.51 -val t = TermC.str2term "Length [1, 1, 1]";
    1.52 +val t = TermC.parse_test @{context} "Length [1, 1, 1]";
    1.53  val t = eval_prog_expr ctxt prog_expr t;
    1.54  case t of 
    1.55    Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => ()