1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Sun Sep 11 14:31:15 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Mon Sep 12 17:46:32 2022 +0200
     1.3 @@ -35,7 +35,8 @@
     1.4  "----------- check return value of adhoc_thm  ----";
     1.5  "----------- check return value of adhoc_thm  ----";
     1.6  val thy = @{theory "Poly"};
     1.7 -val cal = snd (assoc_calc' thy "is_polyexp");
     1.8 +val ctxt = Proof_Context.init_global thy;
     1.9 +val cal = snd (get_calc ctxt "is_polyexp");
    1.10  val t = @{term "(x / x) is_polyexp"};
    1.11  val SOME (thmID, thm) = adhoc_thm ctxt cal t;
    1.12  (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
    1.13 @@ -318,7 +319,7 @@
    1.14  "----------- get_pair with 3 args --------------------------------";
    1.15  val (thy, op_, ef, arg) =
    1.16      (thy, "EqSystem.occur_exactly_in", 
    1.17 -     assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
    1.18 +     get_calc (@{theory "EqSystem"} |> Proof_Context.init_global) "occur_exactly_in" |> snd |> snd,
    1.19       TermC.str2term
    1.20        "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
    1.21        );
    1.22 @@ -345,6 +346,7 @@
    1.23  "----------- fun get_pair: examples ------------------------------------------------------------";
    1.24  "----------- fun get_pair: examples ------------------------------------------------------------";
    1.25  val thy = @{theory};
    1.26 +val ctxt = @{context};
    1.27  val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
    1.28  if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
    1.29  
    1.30 @@ -392,7 +394,7 @@
    1.31  if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
    1.32  then () else error "adhoc_thm  9 is_num  changed";
    1.33  
    1.34 -case assoc_calc thy \<^const_name>\<open>less\<close> of
    1.35 +case get_calc_prog_id ctxt \<^const_name>\<open>less\<close> of
    1.36    "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
    1.37  val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
    1.38  if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
    1.39 @@ -418,7 +420,7 @@
    1.40  if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
    1.41  then () else error "adhoc_thm  6 / -8 = - 3 / 4  changed";
    1.42  
    1.43 -case assoc_calc thy "Prog_Expr.ident" of
    1.44 +case get_calc_prog_id ctxt "Prog_Expr.ident" of
    1.45    "ident" => () | _ => error "Prog_Expr.ident <-> ident  changed";
    1.46  val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
    1.47