1.1 --- a/test/Tools/isac/ProgLang/listC.sml Mon Jun 21 14:39:52 2021 +0200
1.2 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Jun 21 15:36:09 2021 +0200
1.3 @@ -50,8 +50,8 @@
1.4 else error "NTH 1 [a,b,c,d,e] = a ..changed";
1.5
1.6 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
1.7 -val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const ("List.list.Cons", _) $ Free ("a", _) $
1.8 - (Const ("List.list.Cons", _) $ Free ("b", _) $
1.9 +val Const ("ListC.NTH", _) $ Free ("3", _) $ (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
1.10 + (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $
1.11 (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
1.12 TermC.atomty t;
1.13 val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};