1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Tue Aug 10 10:27:15 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Tue Aug 10 11:01:18 2021 +0200
1.3 @@ -472,7 +472,7 @@
1.4 =========================================================================/
1.5
1.6 -----fun refin' ff:
1.7 -> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
1.8 +> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
1.9 [
1.10 (1 ,[1] ,true ,#Given ,Cor equalities
1.11 [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
1.12 @@ -487,7 +487,7 @@
1.13 (true, length_ [c, c_2] = 2)]
1.14
1.15 ----- fun match_oris':
1.16 -> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
1.17 +> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
1.18 > (writeln o pres2str) pre';
1.19 ..as in refin'
1.20
1.21 @@ -554,7 +554,7 @@
1.22
1.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.24 val PblObj {probl,...} = get_obj I pt [5];
1.25 - (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
1.26 + (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
1.27 (*[
1.28 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
1.29 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),