test/Tools/isac/ProgLang/listC.sml
changeset 60309 70a1d102660d
parent 60230 0ca0f9363ad3
child 60331 40eb8aa2b0d6
     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};