1.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml	Sun Jul 31 13:45:20 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml	Sun Jul 31 16:35:33 2022 +0200
     1.3 @@ -205,20 +205,20 @@
     1.4  val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
     1.5  
     1.6  val t = TermC.str2term "x = 0";
     1.7 -val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
     1.8 +val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
     1.9  
    1.10  val t = TermC.str2term "(x + 1) = (x + 1)";
    1.11  val (Const _(*op0,t0*) $ t1 $ t2 ) = t
    1.12 -val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
    1.13 +val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
    1.14  if UnparseC.term t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
    1.15  
    1.16  val t as Const _ $ v $ c = TermC.str2term "1 = 0";
    1.17  val false = variable_constant_pair (v, c);
    1.18 -val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
    1.19 +val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
    1.20  if UnparseC.term t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
    1.21  
    1.22  val t = TermC.str2term "0 = 0";
    1.23 -val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
    1.24 +val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
    1.25  if UnparseC.term t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
    1.26  
    1.27  
    1.28 @@ -422,27 +422,27 @@
    1.29  "-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
    1.30  val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
    1.31  val t = TermC.parseNEW' ctxt  "2 * (3::real)";
    1.32 -(*val SOME (thmid,t') = *)get_pair thy op_ ef t;
    1.33 +(*val SOME (thmid,t') = *)get_pair ctxt op_ ef t;
    1.34  ;
    1.35  "~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
    1.36    (thy, op_, ef, t);
    1.37       (*if*) op_ = op0; (*then*)
    1.38          val popt =
    1.39 -           ef op_ t thy;
    1.40 +           ef op_ t ctxt;
    1.41  "~~~~~ fun eval_binop , args:"; val ((_ : string), (_: string), 
    1.42        (t as (Const (op0, _) $ t1 $ t2)), thy) =
    1.43    ("#mult_", op_, t, thy);
    1.44  val Const (c, _) $ t1 $ t2 =                                               (* binary \<circ> n1 \<circ> n2 *)
    1.45      (*case*) t (*of*);
    1.46        (*if*) is_calcul_op c andalso is_num t1 andalso is_num t2 (*then*);
    1.47 -          val res = calcul thy t;
    1.48 +          val res = calcul ctxt t;
    1.49            val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
    1.50            SOME ("#: " ^ UnparseC.term prop, prop) (*return value*);
    1.51  ;
    1.52  if "#: " ^ UnparseC.term prop = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
    1.53  else error "eval_binop changed"
    1.54  ;
    1.55 -val SOME (thmid, tm) = eval_binop "#mult_"  op_ t thy;
    1.56 +val SOME (thmid, tm) = eval_binop "#mult_"  op_ t ctxt;
    1.57  if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
    1.58  else error "eval_binop changed 2"
    1.59