1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -56,12 +56,12 @@
     1.4  
     1.5  val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
     1.6  case TermC.str2term "NTH 3 [a,b,c,d,e]" of
     1.7 - Const ("ListC.NTH", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $
     1.8 -     (Const ("List.list.Cons", _) $ Free ("a", _) $
     1.9 -       (Const ("List.list.Cons", _) $ Free ("b", _) $
    1.10 -         (Const ("List.list.Cons", _) $ Free ("c", _) $
    1.11 -           (Const ("List.list.Cons", _) $ Free ("d", _) $
    1.12 -             (Const ("List.list.Cons", _) $ Free ("e", _) $ Const ("List.list.Nil", _)))))) => ()
    1.13 + Const (\<^const_name>\<open>NTH\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
    1.14 +     (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $
    1.15 +       (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $
    1.16 +         (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("c", _) $
    1.17 +           (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $
    1.18 +             (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
    1.19  | _ => error "ListC.NTH changed";
    1.20  val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
    1.21  TermC.atomty thm;
    1.22 @@ -105,6 +105,6 @@
    1.23  val t = TermC.str2term "Length [1, 1, 1]";
    1.24  val t = eval_prog_expr thy prog_expr t;
    1.25  case t of 
    1.26 -  Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)) => () 
    1.27 +  Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => () 
    1.28  | _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";
    1.29