1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -48,9 +48,9 @@
     1.4  
     1.5  val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
     1.6  TermC.atomty t;
     1.7 -val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_NIL};
     1.8 +val thm = Thm.prop_of @{thm NTH_NIL};
     1.9  TermC.atomty thm;
    1.10 -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;
    1.11 +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false @{thm NTH_NIL} t;
    1.12  if UnparseC.term t' = "a" then () 
    1.13  else error "NTH 1 [a,b,c,d,e] = a ..changed";
    1.14  
    1.15 @@ -63,9 +63,9 @@
    1.16             (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $
    1.17               (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
    1.18  | _ => error "ListC.NTH changed";
    1.19 -val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
    1.20 +val thm = Thm.prop_of @{thm NTH_CONS};
    1.21  TermC.atomty thm;
    1.22 -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
    1.23 +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false  @{thm NTH_CONS} t;
    1.24  if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
    1.25  else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
    1.26