1.1 --- a/src/Tools/isac/ProgLang/Calculate.thy	Sun Jul 31 13:45:20 2022 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy	Sun Jul 31 16:35:33 2022 +0200
     1.3 @@ -29,22 +29,24 @@
     1.4  val is_calcul_op =
     1.5    member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>realpow\<close>];
     1.6  
     1.7 -fun calcul thy lhs =
     1.8 +fun calcul ctxt lhs =
     1.9    let
    1.10      val simp_ctxt =
    1.11 +(*
    1.12        Proof_Context.init_global thy
    1.13 -      |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
    1.14 -    val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
    1.15 +*)
    1.16 +      ctxt |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
    1.17 +    val eq = Simplifier.rewrite simp_ctxt (Thm.cterm_of ctxt lhs);
    1.18      val rhs = Thm.term_of (Thm.rhs_of eq);
    1.19    in rhs end;
    1.20  
    1.21 -fun eval_binop (_: string) (_: string) t thy =
    1.22 +fun eval_binop (_: string) (_: string) t ctxt =
    1.23    (case t of
    1.24      (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 =>         (* binary \<circ> (v \<circ> n1) \<circ> n2 *)
    1.25        if c1 = c2 andalso is_calcul_op c1 andalso is_num t1 andalso is_num t2 then
    1.26          let
    1.27            val opp' = Const (if c1 = \<^const_name>\<open>minus\<close> then \<^const_name>\<open>plus\<close> else c1, T);
    1.28 -          val res = calcul thy (opp' $ t1 $ t2);
    1.29 +          val res = calcul ctxt (opp' $ t1 $ t2);
    1.30            val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res));
    1.31          in SOME ("#: " ^ UnparseC.term prop, prop) end
    1.32        else NONE
    1.33 @@ -53,7 +55,7 @@
    1.34          andalso is_num t1 andalso is_num t2
    1.35        then
    1.36          let
    1.37 -          val res = calcul thy (opp $ t1 $ t2);
    1.38 +          val res = calcul ctxt (opp $ t1 $ t2);
    1.39            val prop = HOLogic.Trueprop $ HOLogic.mk_eq (t, opp $ res $ v);
    1.40          in
    1.41            SOME ("#: " ^ UnparseC.term prop, prop)
    1.42 @@ -62,7 +64,7 @@
    1.43    | Const (c, _) $ t1 $ t2 =>                                               (* binary \<circ> n1 \<circ> n2 *)
    1.44        if is_calcul_op c andalso is_num t1 andalso is_num t2 then
    1.45          let
    1.46 -          val res = calcul thy t;
    1.47 +          val res = calcul ctxt t;
    1.48            val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
    1.49          in
    1.50            SOME ("#: " ^ UnparseC.term prop, prop)