1.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Mar 18 14:51:58 2020 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Mar 18 15:23:15 2020 +0100
     1.3 @@ -195,12 +195,12 @@
     1.4  
     1.5  fun rules2scr_Rls thy rules =
     1.6      if contain_bdv rules
     1.7 -    then FunID_Term_Bdv $ (Repeat $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
     1.8 -    else FunID_Term $ (Repeat $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term));
     1.9 +    then FunID_Term_Bdv $ (Repeat $ (((op #> o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
    1.10 +    else FunID_Term $ (Repeat $ (((op #> o (map (rule2stac thy))) rules) $ Rule.e_term));
    1.11  fun rules2scr_Seq thy rules =
    1.12      if contain_bdv rules
    1.13 -    then FunID_Term_Bdv $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
    1.14 -    else FunID_Term $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term);
    1.15 +    then FunID_Term_Bdv $ (((op #> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
    1.16 +    else FunID_Term $ (((op #> o (map (rule2stac thy))) rules) $ Rule.e_term);
    1.17  
    1.18  (* REPLACED BY Auto_Prog.gen:
    1.19     prepare the input for an rls for use:
    1.20 @@ -230,6 +230,7 @@
    1.21  
    1.22  (* on the fly generate a Prog from an rls for Math_Engine.detailstep.
    1.23    Types are not precise, but these are not required by LI.
    1.24 +  Argument "thy" is only required for lookup in KEStore.
    1.25  *)
    1.26  fun gen thy t rls =
    1.27    let