1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Mon Apr 19 11:45:43 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Mon Apr 19 15:02:00 2021 +0200
     1.3 @@ -41,28 +41,28 @@
     1.4  "--------------------- NTH ---------------------------------------------------";
     1.5  val prog_expr = assoc_rls "prog_expr"
     1.6  
     1.7 -val t = str2term "NTH 1 [a,b,c,d,e]";
     1.8 -atomty t;
     1.9 +val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
    1.10 +TermC.atomty t;
    1.11  val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_NIL};
    1.12 -atomty thm;
    1.13 +TermC.atomty thm;
    1.14  val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;
    1.15  if UnparseC.term t' = "a" then () 
    1.16  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.17  
    1.18 -val t = str2term "NTH 3 [a,b,c,d,e]";
    1.19 +val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
    1.20  val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
    1.21    (Const ("List.list.Cons", _) $ Free ("b", _) $ 
    1.22      (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
    1.23 -atomty t;
    1.24 +TermC.atomty t;
    1.25  val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
    1.26 -atomty thm;
    1.27 +TermC.atomty thm;
    1.28  val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
    1.29  if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then () 
    1.30  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.31  
    1.32  (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    1.33 -val t = str2term "NTH 3 [a,b,c,d,e]";
    1.34 -atomty t;
    1.35 +val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
    1.36 +TermC.atomty t;
    1.37  Rewrite.trace_on := false;
    1.38  val SOME (t', _) = rewrite_set_ thy false prog_expr t;
    1.39  Rewrite.trace_on := false;
    1.40 @@ -75,7 +75,7 @@
    1.41  val prog_expr = assoc_rls "prog_expr"
    1.42  
    1.43  val thy = @{theory ListC};
    1.44 -val t = str2term "Length [1, 1, 1]";
    1.45 +val t = TermC.str2term "Length [1, 1, 1]";
    1.46  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.47  UnparseC.term t = "1 + Length [1, 1]";
    1.48  val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
    1.49 @@ -88,12 +88,12 @@
    1.50  if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
    1.51  else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
    1.52  
    1.53 -val t = str2term "Length [1, 1, 1]";
    1.54 +val t = TermC.str2term "Length [1, 1, 1]";
    1.55  val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
    1.56  if UnparseC.term t = "3" then ()
    1.57  else error "Length [1, 1, 1] = 3  ..prog_expr changed";
    1.58  
    1.59 -val t = str2term "Length [1, 1, 1]";
    1.60 +val t = TermC.str2term "Length [1, 1, 1]";
    1.61  val t = eval_prog_expr thy prog_expr t;
    1.62  case t of Free ("3", _) => () 
    1.63  | _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";