1.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -389,7 +389,7 @@
     1.4      Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
     1.5  (*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
     1.6  atomt t; term2str t;
     1.7 -val t = rule2stac calclist (Calc ("op +", eval_binop "#add_"));
     1.8 +val t = rule2stac calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
     1.9  atomt t; term2str t;
    1.10  val t = rule2stac [] (Rls_ rearrange_assoc);
    1.11  atomt t; term2str t;
    1.12 @@ -406,7 +406,7 @@
    1.13  			HOLogic.false_const);
    1.14  (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
    1.15  atomt t; term2str t;
    1.16 -val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_"));
    1.17 +val t = rule2stac_inst calclist (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
    1.18  atomt t; term2str t;
    1.19  val t = rule2stac_inst [] (Rls_ rearrange_assoc);
    1.20  atomt t; term2str t;