1.1 --- a/test/Tools/isac/ProgLang/calculate.sml	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/calculate.sml	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  (*  [("Vars",("Tools.Vars",fn)),("Length",("Tools.Length",fn)),
     1.6       ("Nth",("Tools.Nth",fn)),
     1.7 -   ("power_",("Atools.pow",fn)),("plus",("op +",fn)),("times",("op *",fn)),
     1.8 +   ("power_",("Atools.pow",fn)),("plus",("Groups.plus_class.plus",fn)),("times",("op *",fn)),
     1.9     ("is_const",("Atools.is'_const",fn)),
    1.10     ("le",("op <",fn)),("leq",("op <=",fn)),
    1.11     ("ident",("Atools.ident",fn))]                                                      *)
    1.12 @@ -77,9 +77,9 @@
    1.13     ("#Find"  ,["realTestFind s_"])
    1.14     ],
    1.15    {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
    1.16 -   calc=[("plus"    ,("op +"        ,eval_binop "#add_")),
    1.17 +   calc=[("plus"    ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
    1.18  	 ("times"   ,("op *"        ,eval_binop "#mult_")),
    1.19 -	 ("divide_" ,("HOL.divide"  ,eval_cancel "#divide_")),
    1.20 +	 ("divide_" ,("Rings.inverse_class.divide"  ,eval_cancel "#divide_")),
    1.21  	 ("power_"  ,("Atools.pow"  ,eval_binop "#power_"))],
    1.22     crls=tval_rls, nrls=e_rls(*,
    1.23     asm_rls=[],asm_thm=[]*)},
    1.24 @@ -185,7 +185,7 @@
    1.25   trace_rewrite:=true;
    1.26   val thy = Test.thy;
    1.27   val t = (term_of o the o (parse thy)) "(-4) / 2";
    1.28 - val SOME (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
    1.29 + val SOME (_,t) = eval_cancel "xxx" "Rings.inverse_class.divide" t thy;
    1.30   term2str t;
    1.31  "-4 / 2 = (-2)";
    1.32  (*-------------- but ... *)