1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Thu Sep 16 12:23:57 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Thu Sep 16 17:23:54 2021 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
     1.5  val plus =   ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
     1.6  val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
     1.7 -val pow =    ("Transcendental.powr", eval_binop "#power_") : string * Eval_Def.eval_fn;
     1.8 +val pow =    (\<^const_name>\<open>realpow\<close>, eval_binop "#power_") : string * Eval_Def.eval_fn;
     1.9  
    1.10  "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
    1.11  val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
    1.12 @@ -269,7 +269,7 @@
    1.13  
    1.14    val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
    1.15    (*
    1.16 -val op_ = \<^const_name>\<open>powr\<close> : string
    1.17 +val op_ = \<^const_name>\<open>realpow\<close> : string
    1.18  val eval_fn = fn : string -> term -> theory -> (string * term) option*)
    1.19  
    1.20    val SOME (thmid,t') = get_pair thy op_ eval_fn t;
    1.21 @@ -279,8 +279,8 @@
    1.22  (*** calc: operator = pow not defined*)
    1.23  
    1.24  case (op_, t) of
    1.25 -  ("Transcendental.powr",
    1.26 -    Const (\<^const_name>\<open>powr\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
    1.27 +  (\<^const_name>\<open>realpow\<close>,
    1.28 +    Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
    1.29        (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
    1.30  | _ => error "3 \<up> 2 CHANGED";
    1.31    val SOME (id, t') = eval_binop thmid op_ t thy;