1.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Fri Feb 09 11:16:05 2018 +0100
     1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Fri Feb 09 11:45:53 2018 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4                  > nxt_specify_init_calc 
     1.5                  > prep_ori
     1.6  *)
     1.7 -val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
     1.8 +val (thy, pbt) = (Thy_Info_get_theory thyID, (#ppc o get_pbt) pblID);
     1.9  "----- in  prep_ori";
    1.10  val ctxt = Proof_Context.init_global thy;
    1.11  
    1.12 @@ -441,7 +441,7 @@
    1.13      val thy = assoc_thy dI;
    1.14  	    val {ppc, ...} = get_met mI;
    1.15  (*  val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
    1.16 -val ctxt' = dI |> Thy_Info.get_theory |> Proof_Context.init_global;
    1.17 +val ctxt' = dI |> Thy_Info_get_theory |> Proof_Context.init_global;
    1.18  (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]); 
    1.19                                                 ^^^^^ *)
    1.20  (*vvv from:  | assod pt _ (Subproblem'...*)

     2.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Fri Feb 09 11:16:05 2018 +0100
     2.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Fri Feb 09 11:45:53 2018 +0100
     2.3 @@ -57,7 +57,7 @@
     2.4                   :
     2.5                   case assod pt d m stac of
     2.6  "~~~~~ fun assod, args:"; val (...Subproblem'...) = ();
     2.7 -	      val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 
     2.8 +	      val ctxt = dI |> Thy_Info_get_theory |> Proof_Context.init_global 
     2.9            |> declare_constraints' vals
    2.10  *)
    2.11  

     3.1 --- a/test/Tools/isac/ProgLang/calculate.sml	Fri Feb 09 11:16:05 2018 +0100
     3.2 +++ b/test/Tools/isac/ProgLang/calculate.sml	Fri Feb 09 11:45:53 2018 +0100
     3.3 @@ -362,7 +362,7 @@
     3.4  "----------- get_pair with 3 args --------------------------------";
     3.5  val (thy, op_, ef, arg) =
     3.6      (thy, "EqSystem.occur'_exactly'_in", 
     3.7 -     assoc_calc' (Thy_Info.get_theory "EqSystem") "occur_exactly_in" |> snd |> snd,
     3.8 +     assoc_calc' (Thy_Info_get_theory "EqSystem") "occur_exactly_in" |> snd |> snd,
     3.9       str2term
    3.10        "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
    3.11        );

     4.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Feb 09 11:16:05 2018 +0100
     4.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri Feb 09 11:45:53 2018 +0100
     4.3 @@ -124,8 +124,421 @@
     4.4    ML_file          "kestore.sml"        (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
     4.5    ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
     4.6    ML_file "ProgLang/termC.sml"
     4.7 +
     4.8 +ML {*
     4.9 +*} ML {*
    4.10 +(* Title:  test calculation of values for function constants
    4.11 +   Author: Walther Neuper 2000
    4.12 +   (c) copyright due to lincense terms.
    4.13 +
    4.14 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
    4.15 +        10        20        30        40        50        60        70        80
    4.16 +*)
    4.17 +
    4.18 +"--------------------------------------------------------";
    4.19 +"table of contents --------------------------------------";
    4.20 +"--------------------------------------------------------";
    4.21 +"-calculate.thy: provides 'setup' -----------------------";
    4.22 +"----------- fun norm -----------------------------------";
    4.23 +"----------- check return value of adhoc_thm  ----";
    4.24 +"----------- fun calculate_ -----------------------------";
    4.25 +"----------- calculate from script --requires 'setup'----";
    4.26 +"----------- calculate check test-root-equ --------------";
    4.27 +"----------- check calcul,ate bottom up -----------------";
    4.28 +"----------- Atools.pow Power.power_class.power ---------";
    4.29 +" ================= calculate.sml: calculate_ 2002 ======";
    4.30 +"----------- get_pair with 3 args -----------------------";
    4.31 +"----------- calculate (2 * x is_const) -----------------";
    4.32 +"--------------------------------------------------------";
    4.33 +"--------------------------------------------------------";
    4.34 +"--------------------------------------------------------";
    4.35 +
    4.36 +"----------- check return value of adhoc_thm  ----";
    4.37 +"----------- check return value of adhoc_thm  ----";
    4.38 +"----------- check return value of adhoc_thm  ----";
    4.39 +val thy = @{theory "Poly"};
    4.40 +val cal = snd (assoc_calc' thy "is_polyexp");
    4.41 +val t = @{term "(x / x) is_polyexp"};
    4.42 +val SOME (thmID, thm) = adhoc_thm thy cal t;
    4.43 +(HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
    4.44 +handle TERM _ => 
    4.45 +       error "calculate.sml: adhoc_thm must return Trueprop";
    4.46 +
    4.47 +"----------- fun calculate_ -----------------------------";
    4.48 +"----------- fun calculate_ -----------------------------";
    4.49 +"----------- fun calculate_ -----------------------------";
    4.50 +val thy = @{theory "Test"};
    4.51 +"===== test 1";
    4.52 +val t = (Thm.term_of o the o (parse thy)) "1+2";
    4.53 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
    4.54 +term2str (Thm.prop_of thm) = "1 + 2 = 3";
    4.55 +
    4.56 +"===== test 2";
    4.57 +val t = (Thm.term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
    4.58 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
    4.59 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    4.60 +if term2str t = "(3 * 4 / 3) ^^^ 2" then ()
    4.61 +else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2";
    4.62 +
    4.63 +"===== test 3b -- 2 contiued";
    4.64 +val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t;
    4.65 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    4.66 +term2str t;
    4.67 +(*val it = "(#12 // #3) ^^^ #2" : string*)
    4.68 +
    4.69 +"===== test 4";
    4.70 +val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
    4.71 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    4.72 +term2str t;
    4.73 +(*it = "#4 ^^^ #2" : string*)
    4.74 +
    4.75 +"===== test 5";
    4.76 +val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
    4.77 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    4.78 +(*show_types := false;*)
    4.79 +if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"
    4.80 +else ();
    4.81 +
    4.82 +
    4.83 +val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
    4.84 +val (dI',pI',mI') =
    4.85 +  ("Test",["calculate","test"],["Test","test_calculate"]);
    4.86 +
    4.87 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    4.88 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.89 +(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
    4.90 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.91 +(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
    4.92 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.93 +(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
    4.94 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.95 +(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
    4.96 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.97 +(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
    4.98 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.99 +(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
   4.100 +
   4.101 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   4.102 +(*nxt = ("Calculate",Calculate "PLUS")*)
   4.103 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   4.104 +(*nxt = ("Calculate",Calculate "TIMES")*)
   4.105 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   4.106 +(*nxt = ("Calculate",Calculate "DIVIDE")*)
   4.107 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   4.108 +(*nxt = ("Calculate",Calculate "POWER")*)
   4.109 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   4.110 +(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
   4.111 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   4.112 +(*nxt = ("End_Proof'",End_Proof')*)
   4.113 +case f of FormKF "16" => () | _ =>
   4.114 +error "calculate.sml: script test_calculate changed behaviour";
   4.115 +
   4.116 +
   4.117 +"----------- calculate check test-root-equ --------------";
   4.118 +"----------- calculate check test-root-equ --------------";
   4.119 +"----------- calculate check test-root-equ --------------";
   4.120 +(*(1): 2nd Test_simplify didn't work:
   4.121 +val ct =
   4.122 +  "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
   4.123 +> val rls = ("Test_simplify");
   4.124 +> val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
   4.125 +val ct = "sqrt (x ^^^ 2 + -3 * x) =
   4.126 +(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
   4.127 +ie. cancel does not work properly
   4.128 +*)
   4.129 + val thy = "Test";
   4.130 + val op_ = "DIVIDE";
   4.131 + val ct = "sqrt (x ^^^ 2 + -3 * x) =\
   4.132 + \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
   4.133 + val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
   4.134 + writeln ct;
   4.135 +(*
   4.136 +           sqrt (x ^^^ 2 + -3 * x) =\
   4.137 + \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
   4.138 +............... does not work *)
   4.139 +
   4.140 +(*--------------(2): does divide work in Test_simplify ?: ------*)
   4.141 + val thy = @{theory Test};
   4.142 + val t = (Thm.term_of o the o (parse thy)) "6 / 2";
   4.143 + val rls = Test_simplify;
   4.144 + val (t,_) = the (rewrite_set_ thy false rls t);
   4.145 +(*val t = Free ("3","Real.real") : term*)
   4.146 +
   4.147 + val thy = "Test";
   4.148 + val t = "6 / 2";
   4.149 + val rls = "Test_simplify";
   4.150 + val (t,_) = the (rewrite_set thy false rls t);
   4.151 +(*val t = "3" : string
   4.152 +      ....... works, thus: which rule in SqRoot_simplify works differently ?*)
   4.153 +
   4.154 +
   4.155 +(*--------------(3): is_const works ?: -------------------------------------*)
   4.156 + val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
   4.157 + atomty t;
   4.158 + rewrite_set_ @{theory Test} false tval_rls t;
   4.159 +(*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
   4.160 +
   4.161 + val t = str2term "2 * x is_const";
   4.162 + val SOME (str,t') = eval_const "" "" t (@{theory "Isac"});
   4.163 + term2str t';
   4.164 + 
   4.165 +
   4.166 +"----------- check calculate bottom up ------------------";
   4.167 +"----------- check calculate bottom up ------------------";
   4.168 +"----------- check calculate bottom up ------------------";
   4.169 +(*-------------- eval_cancel works: *)
   4.170 + trace_rewrite:=false;
   4.171 + val thy = @{theory Test};
   4.172 + val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
   4.173 +
   4.174 +val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
   4.175 +
   4.176 + term2str t;
   4.177 +"-4 / 2 = (-2)";
   4.178 +(*-------------- but ... *)
   4.179 + val ct = "x + (-4) / 2";
   4.180 +
   4.181 +val thy' = "Test"; (* added AK110727 *)
   4.182 + val (ct,_) = the (rewrite_set thy' false rls ct);
   4.183 +
   4.184 +"(-2) + x";
   4.185 +(*-------------- while ... *)
   4.186 + val ct = "(-4) / 2";
   4.187 +
   4.188 + val (ct,_) = the (rewrite_set thy'  false rls ct);
   4.189 +
   4.190 +"-2";
   4.191 +*} ML {*
   4.192 +
   4.193 +(*--------------(5): reproduce (1) with simpler term: ------------*)
   4.194 + val thy = "Test";
   4.195 + val t = "(3+5)/2";
   4.196 + val (t,_) = the (rewrite_set thy false rls t);
   4.197 +(*val t = "4" ... works*)
   4.198 +
   4.199 + val t = "(3+1+2*x)/2";
   4.200 + val (t,_) = the (rewrite_set thy false rls t);
   4.201 +(*val t = "2 + x" ... works*)
   4.202 +
   4.203 + trace_rewrite:=false; (*=true3.6.03*)
   4.204 +
   4.205 + val thy = "Test";
   4.206 + val rls = "Test_simplify";
   4.207 + val t = "(3+(1+2*x))/2";
   4.208 + val (t,_) = the (rewrite_set thy false rls t);
   4.209 +(*val t = "2 + x" ... works: give up----------------------------------------*)
   4.210 + trace_rewrite:=false; 
   4.211 +
   4.212 + trace_rewrite:=false; (*=true3.6.03*)
   4.213 + val thy = @{theory Test};
   4.214 + val rls = Test_simplify;
   4.215 + val t = str2term "(3+(1+2*x))/2";
   4.216 + val SOME (t',asm) = rewrite_set_ thy false rls t;
   4.217 + term2str t';
   4.218 +(*val t = "2 + x" ... works: give up----------------------------------------*)
   4.219 + trace_rewrite:=false; 
   4.220 +
   4.221 +
   4.222 +
   4.223 +
   4.224 +(*--- trace_rewrite before correction of ... --------------------
   4.225 + val ct = "(-3 + 2 * x + -1) / 2";
   4.226 + val (ct,_) = the (rewrite_set thy'  false rls ct);
   4.227 +:
   4.228 +### trying thm 'root_ge0_2'
   4.229 +### rewrite_set_: x + (-1 + -3) / 2
   4.230 +### trying thm 'radd_real_const_eq'
   4.231 +### trying thm 'radd_real_const'
   4.232 +### rewrite_set_: x + (-4) / 2
   4.233 +### trying thm 'rcollect_right'
   4.234 +:
   4.235 +"x + (-4) / 2"
   4.236 +-------------------------------------while before Isabelle20002:
   4.237 + val ct = "(#-3 + #2 * x + #-1) // #2";
   4.238 + val (ct,_) = the (rewrite_set thy'  false rls ct);
   4.239 +:
   4.240 +### trying thm 'root_ge0_2'
   4.241 +### rewrite_set_: x + (#-1 + #-3) // #2
   4.242 +### trying thm 'radd_real_const_eq'
   4.243 +### trying thm 'radd_real_const'
   4.244 +### rewrite_set_: x + #-4 // #2
   4.245 +### rewrite_set_: x + #-2
   4.246 +### trying thm 'rcollect_right'
   4.247 +:
   4.248 +"#-2 + x"
   4.249 +-----------------------------------------------------------------*)
   4.250 +
   4.251 +
   4.252 +(*===================*)
   4.253 + trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
   4.254 + val thy' = "Test";
   4.255 + val rls = "Test_simplify";		
   4.256 + val ct = "x + (-1 + -3) / 2";
   4.257 + val (ct,_) = the (rewrite_set thy'  false rls ct);	
   4.258 +"x + (-4) / 2";						
   4.259 +(*
   4.260 +### trying calc. 'cancel'
   4.261 +@@@ get_pair: binop, t = x + (-4) / 2
   4.262 +@@@ get_pair: t else
   4.263 +@@@ get_pair: t else -> NONE
   4.264 +@@@ get_pair: binop, t = (-4) / 2
   4.265 +@@@ get_pair: then 1
   4.266 +@@@ get_pair: t -> NONE
   4.267 +@@@ get_pair: t1 -> NONE
   4.268 +@@@ adhoc_thm': NONE
   4.269 +### trying calc. 'pow'
   4.270 +*)
   4.271 +*} ML {*
   4.272 +
   4.273 + trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
   4.274 + val thy' = "Test";
   4.275 + val rls = "Test_simplify";		
   4.276 + val ct = "x + (-4) / 2";
   4.277 + val (ct,_) = the (rewrite_set thy'  false rls ct);	
   4.278 +"(-2) + x";
   4.279 +(*
   4.280 +### trying calc. 'cancel'
   4.281 +@@@ get_pair: binop, t = x + -4 / 2
   4.282 +@@@ get_pair: t else
   4.283 +@@@ get_pair: t else -> NONE
   4.284 +@@@ get_pair: binop, t = -4 / 2
   4.285 +@@@ get_pair: then 1
   4.286 +@@@ adhoc_thm': SOME #cancel_-4_2
   4.287 +### calc. to: x + (-2)
   4.288 +### trying calc. 'cancel'
   4.289 +*)
   4.290 + trace_rewrite:=false;
   4.291 +
   4.292 +"----------- Atools.pow Power.power_class.power ---------";
   4.293 +"----------- Atools.pow Power.power_class.power ---------";
   4.294 +"----------- Atools.pow Power.power_class.power ---------";
   4.295 +val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
   4.296 +atomty t;
   4.297 +(*** -------------
   4.298 +*** Const ( Nat.power, ['a, nat] => 'a)
   4.299 +*** . Free ( 1, 'a)
   4.300 +*** . Free ( aaa, nat) *)
   4.301 +
   4.302 +val t = str2term "1 ^^^ aaa";
   4.303 +atomty t;
   4.304 +(**** 
   4.305 +*** Const (Atools.pow, real => real => real)
   4.306 +*** . Free (1, real)
   4.307 +*** . Free (aaa, real)
   4.308 +*** *);
   4.309 +
   4.310 +" ================= calculate.sml: calculate_ 2002 =================== ";
   4.311 +" ================= calculate.sml: calculate_ 2002 =================== ";
   4.312 +" ================= calculate.sml: calculate_ 2002 =================== ";
   4.313 +
   4.314 +val thy = @{theory Test};
   4.315 +val t = (Thm.term_of o the o (parse thy)) "12 / 3";
   4.316 +val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
   4.317 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
   4.318 +"12 / 3 = 4";
   4.319 +val thy = @{theory Test};
   4.320 +val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2";
   4.321 +val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER"))) t;
   4.322 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
   4.323 +"4 ^ 2 = 16";
   4.324 +
   4.325 + val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
   4.326 + val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t;
   4.327 +"1 + 2 = 3";
   4.328 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
   4.329 + term2str t;
   4.330 +"(3 * 4 / 3) ^^^ 2";
   4.331 + val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES")))t;
   4.332 +"3 * 4 = 12";
   4.333 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
   4.334 + term2str t;
   4.335 +"(12 / 3) ^^^ 2";
   4.336 + val SOME (thmID,thm) =adhoc_thm thy(the(assoc(calclist,"DIVIDE")))t;
   4.337 +"12 / 3 = 4";
   4.338 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
   4.339 + term2str t;
   4.340 +"4 ^^^ 2";
   4.341 + val SOME (thmID,thm) = adhoc_thm thy(the(assoc(calclist,"POWER")))t;
   4.342 +"4 ^^^ 2 = 16";
   4.343 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
   4.344 + term2str t;
   4.345 +"16";
   4.346 + if it <> "16" then error "calculate.sml: new behaviour in calculate_"
   4.347 + else ();
   4.348 +*} ML {*
   4.349 +
   4.350 +(*13.9.02 *** calc: operator = pow not defined*)
   4.351 +  val t = (Thm.term_of o the o (parse thy)) "3^^^2";
   4.352 +  val SOME (thmID,thm) = 
   4.353 +      adhoc_thm thy (the(assoc(calclist,"POWER"))) t;
   4.354 +(*** calc: operator = pow not defined*)
   4.355 +
   4.356 +  val (op_, eval_fn) = the (assoc(calclist,"POWER"));
   4.357 +  (*
   4.358 +val op_ = "Atools.pow" : string
   4.359 +val eval_fn = fn : string -> term -> theory -> (string * term) option*)
   4.360 +
   4.361 +  val SOME (thmid,t') = get_pair thy op_ eval_fn t;
   4.362 +(*** calc: operator = pow not defined*)
   4.363 +
   4.364 +  val SOME (id,t') = eval_fn op_ t thy;
   4.365 +(*** calc: operator = pow not defined*)
   4.366 +
   4.367 +  val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
   4.368 +  val SOME (id,t') = eval_binop thmid op_ t thy;
   4.369 +(*** calc: operator = pow not defined*)
   4.370 +
   4.371 +*} ML {*
   4.372 +@{theory EqSystem}; (*.., Isac.EqSystem}*)
   4.373 +*} ML {*
   4.374 +*} ML {*
   4.375 +*} ML {*
   4.376 +*} ML {*
   4.377 +*} ML {*
   4.378 +*} ML {*
   4.379 +*} ML {* (*Theory loader: undefined entry for theory "EqSystem"*)
   4.380 +
   4.381 +"----------- get_pair with 3 args --------------------------------";
   4.382 +"----------- get_pair with 3 args --------------------------------";
   4.383 +"----------- get_pair with 3 args --------------------------------";
   4.384 +val (thy, op_, ef, arg) =
   4.385 +    (thy, "EqSystem.occur'_exactly'_in", 
   4.386 +     assoc_calc' (Thy_Info_get_theory "EqSystem") "occur_exactly_in" |> snd |> snd,
   4.387 +     str2term
   4.388 +      "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
   4.389 +      );
   4.390 +val SOME (str, simpl) = get_pair thy op_ ef arg;
   4.391 +*} ML {*
   4.392 +*} ML {*
   4.393 +*} ML {*
   4.394 +*} ML {*
   4.395 +*} ML {*
   4.396 +*} ML {*
   4.397 +*} ML {*
   4.398 +if str = "2 * x_" then () else writeln "probably WORKS"
   4.399 +*} text {*
   4.400 +if str = 
   4.401 +"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
   4.402 +then () else error "calculate.sml get_pair with 3 args:occur_exactly_in";
   4.403 +*} ML {*
   4.404 +
   4.405 +
   4.406 +"----------- calculate (2 * x is_const) -----------------";
   4.407 +"----------- calculate (2 * x is_const) -----------------";
   4.408 +"----------- calculate (2 * x is_const) -----------------";
   4.409 +val t = str2term "2 * x is_const";
   4.410 +val SOME (str, t') = eval_const "" "" t @{theory Test};
   4.411 +term2str t';
   4.412 +"(2 * x is_const) = False";
   4.413 +
   4.414 +val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
   4.415 +term2str t';
   4.416 +"HOL.False";
   4.417 +
   4.418 +*} ML {*
   4.419 +*}
   4.420 +(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
   4.421    ML_file "ProgLang/calculate.sml"      (* requires setup from calculate.thy                    *)
   4.422 -(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
   4.423    ML_file "ProgLang/rewrite.sml"
   4.424    ML_file "ProgLang/listC.sml"
   4.425    ML_file "ProgLang/scrtools.sml"

     5.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml	Fri Feb 09 11:16:05 2018 +0100
     5.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml	Fri Feb 09 11:45:53 2018 +0100
     5.3 @@ -35,13 +35,13 @@
     5.4  (*val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]; 
     5.5    (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
     5.6  "~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
     5.7 -(*get_py  (Thy_Info.get_theory "Pure") theID theID (get_thes ()); 
     5.8 +(*get_py  (Thy_Info_get_theory "Pure") theID theID (get_thes ()); 
     5.9    (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
    5.10  (*default_print_depth 3; 999*)
    5.11  (get_thes ());
    5.12  
    5.13 -(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info.get_theory "Pure"), theID, theID, (get_thes ()));*)
    5.14 -"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((Thy_Info.get_theory "Pure"), theID, theID, (get_thes ()));
    5.15 +(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info_get_theory "Pure"), theID, theID, (get_thes ()));*)
    5.16 +"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((Thy_Info_get_theory "Pure"), theID, theID, (get_thes ()));
    5.17  error ("get_pbt not found: "^(strs2str d));
    5.18  (*AK110725 To be continued...s*)
    5.19  *)

     6.1 --- a/test/Tools/isac/xmlsrc/mathml.sml	Fri Feb 09 11:16:05 2018 +0100
     6.2 +++ b/test/Tools/isac/xmlsrc/mathml.sml	Fri Feb 09 11:45:53 2018 +0100
     6.3 @@ -48,14 +48,14 @@
     6.4  (*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
     6.5                     Failed to parse term*)*)
     6.6  "~~~~~ fun str2term, args:"; val (str) = (str);
     6.7 -Thy_Info.get_theory "Isac";
     6.8 +Thy_Info_get_theory "Isac";
     6.9  
    6.10  parse_patt;
    6.11 -parse_patt (Thy_Info.get_theory "Isac");
    6.12 -(*parse_patt (Thy_Info.get_theory "Isac") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    6.13 +parse_patt (Thy_Info_get_theory "Isac");
    6.14 +(*parse_patt (Thy_Info_get_theory "Isac") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
    6.15  Failed to parse term*)*)
    6.16  
    6.17 -"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info.get_theory "Isac"), str);
    6.18 +"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info_get_theory "Isac"), str);
    6.19  (thy, str) 
    6.20  |>> thy2ctxt
    6.21  (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"

     7.1 --- a/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml	Fri Feb 09 11:16:05 2018 +0100
     7.2 +++ b/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml	Fri Feb 09 11:45:53 2018 +0100
     7.3 @@ -144,7 +144,7 @@
     7.4  "----- fun pbl2term ----------------------------------------------";
     7.5  "----- fun pbl2term ----------------------------------------------";
     7.6  (*see WN120405a.TODO.txt*)
     7.7 -if term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]) =
     7.8 +if term2str (pbl2term (Thy_Info_get_theory "Isac") ["equations","univariate","normalize"]) =
     7.9    "Problem (Isac', [normalize, univariate, equations])"
    7.10  then () else error "fun pbl2term changed";
    7.11