1.1 --- a/src/Tools/isac/ProgLang/Calculate.thy	Thu Sep 23 13:47:16 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy	Fri Sep 24 14:18:10 2021 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4      val _ = tracing ("-----calcul: lhs = " ^ UnparseC.term lhs)
     1.5      val simp_ctxt =
     1.6        Proof_Context.init_global thy
     1.7 -      |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main});
     1.8 +      |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
     1.9      val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
    1.10      val rhs = Thm.term_of (Thm.rhs_of eq);
    1.11      val _ = tracing ("=====calcul: rhs = " ^ UnparseC.term rhs)(* \<^assert> (is_num rhs);*)

     2.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Thu Sep 23 13:47:16 2021 +0200
     2.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Fri Sep 24 14:18:10 2021 +0200
     2.3 @@ -305,7 +305,7 @@
     2.4  "~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t);
     2.5      val simp_ctxt =
     2.6        Proof_Context.init_global thy
     2.7 -      |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main});
     2.8 +      |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
     2.9      val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
    2.10  
    2.11  if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";

     3.1 --- a/test/Tools/isac/Test_Some.thy	Thu Sep 23 13:47:16 2021 +0200
     3.2 +++ b/test/Tools/isac/Test_Some.thy	Fri Sep 24 14:18:10 2021 +0200
     3.3 @@ -123,7 +123,7 @@
     3.4    if-then-else \<and> < \<ge> even_real odd_real are possible reasons for insufficiency.
     3.5  *)
     3.6  val t = calcul @{theory} @{term "4 \<up> 2 ::real"};
     3.7 -if UnparseC.term_in_ctxt @{context} t = "4 \<up> 2"
     3.8 +if UnparseC.term_in_ctxt @{context} t = "16"
     3.9  then () else error "calcul  4 \<up> 2 \<longrightarrow> 16  corrected ? ";
    3.10  \<close> ML \<open>
    3.11