1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Sun Jul 31 13:45:20 2022 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Sun Jul 31 16:35:33 2022 +0200
     1.3 @@ -268,10 +268,10 @@
     1.4  val op_ = \<^const_name>\<open>realpow\<close> : string
     1.5  val eval_fn = fn : string -> term -> theory -> (string * term) option*)
     1.6  
     1.7 -  val SOME (thmid,t') = get_pair thy op_ eval_fn t;
     1.8 +  val SOME (thmid,t') = get_pair ctxt op_ eval_fn t;
     1.9  (*** calc: operator = pow not defined*)
    1.10  
    1.11 -  val SOME (id,t') = eval_fn op_ t thy;
    1.12 +  val SOME (id,t') = eval_fn op_ t ctxt;
    1.13  (*** calc: operator = pow not defined*)
    1.14  
    1.15  case (op_, t) of
    1.16 @@ -279,7 +279,7 @@
    1.17      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.18        (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
    1.19  | _ => error "3 \<up> 2 CHANGED";
    1.20 -  val SOME (id, t') = eval_binop thmid op_ t thy;
    1.21 +  val SOME (id, t') = eval_binop thmid op_ t ctxt;
    1.22  (*** calc: operator = pow not defined*)
    1.23  
    1.24  if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop  3 \<up> 2 = 9  CHANGED";
    1.25 @@ -322,7 +322,7 @@
    1.26       TermC.str2term
    1.27        "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
    1.28        );
    1.29 -val SOME (str, simpl) = get_pair thy op_ ef arg;
    1.30 +val SOME (str, simpl) = get_pair ctxt op_ ef arg;
    1.31  if str = 
    1.32  "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True"
    1.33  then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
    1.34 @@ -349,36 +349,36 @@
    1.35  if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
    1.36  
    1.37  val t = @{term "3 + 4 :: real"};
    1.38 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
    1.39 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
    1.40  (*+*)if str =  "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
    1.41  (*+*)then () else error "get_pair  3 + 4  changed";
    1.42  
    1.43  val t = @{term "(a + 3) + 4 :: real"};
    1.44 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
    1.45 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
    1.46  if str =  "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
    1.47  then () else error "get_pair  (a + 3) + 4  changed";
    1.48  
    1.49  val t = @{term "(a + 3) + 4 :: real"};
    1.50 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
    1.51 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
    1.52  if str =  "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
    1.53  then () else error "get_pair  (a + 3) + 4  changed";
    1.54  
    1.55  val t = @{term "x = 5 * (3 + (4 + a) :: real)"};
    1.56 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
    1.57 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
    1.58  if str =  "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
    1.59  then ((* !!! gets subterm !!!*)) else error "get_pair  x = 5 * (3 + (4 + a))  (subterm) changed";
    1.60  
    1.61  val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
    1.62  
    1.63  val t = @{term "-4 / - 2 :: real"};
    1.64 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
    1.65 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
    1.66  if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
    1.67  then () else error "get_pair  -4 / - 2   changed";
    1.68  
    1.69  val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
    1.70  
    1.71  val t = @{term "2 \<up> 3 :: real"};
    1.72 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
    1.73 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
    1.74  if str =  "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
    1.75  then () else error "get_pair  2 \<up> 3   changed";
    1.76  
    1.77 @@ -452,7 +452,7 @@
    1.78  "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
    1.79  val SOME
    1.80      ("#divide_e~1_2", t'') =
    1.81 -  (*case*) get_pair thy op_ eval_fn t (*of*);
    1.82 +  (*case*) get_pair ctxt op_ eval_fn t (*of*);
    1.83  (*
    1.84    get_pair finds two adjacent numerals and does NOT distinguish between different kinds of 
    1.85    \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input..
    1.86 @@ -463,7 +463,7 @@
    1.87  val NONE = adhoc_thm @{theory} eval_ t;
    1.88  "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
    1.89  val NONE =
    1.90 -  (*case*) get_pair thy op_ eval_fn t (*of*);
    1.91 +  (*case*) get_pair ctxt op_ eval_fn t (*of*);
    1.92  
    1.93  
    1.94  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.95 @@ -474,10 +474,10 @@
    1.96  
    1.97  "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
    1.98    ((ThyC.get_theory "Isac_Knowledge"),
    1.99 -    ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);
   1.100 +    ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t);
   1.101  
   1.102  val SOME (thmid, t) =
   1.103 -  (*case*) get_pair thy op_ eval_fn ct (*of*);
   1.104 +  (*case*) get_pair ctxt op_ eval_fn ct (*of*);
   1.105  (*+*)val "sqrt 4 = 2" = UnparseC.term t;
   1.106  
   1.107  (** )