1.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml	Tue Aug 10 10:27:15 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml	Tue Aug 10 11:01:18 2021 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  
     1.5  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     1.6  val PblObj {probl,...} = get_obj I pt [5];
     1.7 -    (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
     1.8 +    (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
     1.9  (*[
    1.10  (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.11  (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),