test/Tools/isac/ProgLang/auto_prog.sml
changeset 60565 f92963a33fe3
parent 60559 aba19e46dd84
child 60571 19a172de0bb5
     1.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -51,9 +51,9 @@
     1.4  if UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]"
     1.5  then () else error "formal_args of auto-gen.script changed";
     1.6  
     1.7 -    Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.str2term "someTermWithBdv");
     1.8 +    Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.parse_test @{context} "someTermWithBdv");
     1.9  "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
    1.10 -  = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.str2term "someTermWithBdv");
    1.11 +  = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.parse_test @{context} "someTermWithBdv");
    1.12        val v = case Subst.T_from_input ctxt subs of
    1.13          (_, v) :: _ => v;
    1.14      (*case*) get_rls ctxt rls (*of*);