1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Sat Apr 17 20:44:57 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Sat Apr 17 21:10:27 2021 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  val t = str2term "NTH 1 [a,b,c,d,e]";
     1.6  atomty t;
     1.7 -val thm = (#prop o Thm.rep_thm o ThmC.numerals_to_Free) @{thm NTH_NIL};
     1.8 +val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_NIL};
     1.9  atomty thm;
    1.10  val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;
    1.11  if UnparseC.term t' = "a" then () 
    1.12 @@ -54,7 +54,7 @@
    1.13    (Const ("List.list.Cons", _) $ Free ("b", _) $ 
    1.14      (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
    1.15  atomty t;
    1.16 -val thm = (#prop o Thm.rep_thm o ThmC.numerals_to_Free) @{thm NTH_CONS};
    1.17 +val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
    1.18  atomty thm;
    1.19  val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
    1.20  if UnparseC.term t' = "NTH (3 + -1) [b, c, d, e]" then ()