test/Tools/isac/ProgLang/listC.sml
changeset 60543 9555ee96e046
parent 60509 2e0b7ca391dc
child 60565 f92963a33fe3
     1.1 --- a/test/Tools/isac/ProgLang/listC.sml	Tue Sep 06 11:47:00 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Wed Sep 07 10:58:12 2022 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  "--------------------- NTH ---------------------------------------------------";
     1.5  "--------------------- NTH ---------------------------------------------------";
     1.6  val ctxt = Proof_Context.init_global @{theory}
     1.7 -val prog_expr = assoc_rls "prog_expr"
     1.8 +val prog_expr = get_rls @{context} "prog_expr"
     1.9  
    1.10  val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
    1.11  TermC.atomty t;
    1.12 @@ -81,7 +81,7 @@
    1.13  "--------------------- Length ------------------------------------------------";
    1.14  "--------------------- Length ------------------------------------------------";
    1.15  "--------------------- Length ------------------------------------------------";
    1.16 -val prog_expr = assoc_rls "prog_expr"
    1.17 +val prog_expr = get_rls @{context} "prog_expr"
    1.18  
    1.19  val thy = @{theory ListC};
    1.20  val t = TermC.str2term "Length [1, 1, 1]";