1.1 --- a/test/Tools/isac/IsacKnowledge/eqsystem.sml	Tue Aug 17 09:05:51 2010 +0200
     1.2 +++ b/test/Tools/isac/IsacKnowledge/eqsystem.sml	Wed Aug 18 13:40:09 2010 +0200
     1.3 @@ -813,7 +813,7 @@
     1.4  
     1.5  
     1.6  -----fun refin' ff:
     1.7 -> (writeln o (itms2str Isac.thy)) itms;
     1.8 +> (writeln o (itms2str_ (thy2ctxt "Isac"))) itms;
     1.9  [
    1.10  (1 ,[1] ,true ,#Given ,Cor equalities
    1.11   [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
    1.12 @@ -828,7 +828,7 @@
    1.13  (true, length_ [c, c_2] = 2)]
    1.14  
    1.15  ----- fun match_oris':
    1.16 -> (writeln o (itms2str Isac.thy)) itms;
    1.17 +> (writeln o (itms2str_ (thy2ctxt "Isac"))) itms;
    1.18  > (writeln o pres2str) pre';
    1.19  ..as in refin'
    1.20  
    1.21 @@ -895,7 +895,8 @@
    1.22    | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
    1.23  
    1.24  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.25 -val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;
    1.26 +val PblObj {probl,...} = get_obj I pt [5];
    1.27 +    (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
    1.28  (*[
    1.29  (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
    1.30  (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
    1.31 @@ -963,7 +964,8 @@
    1.32    | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
    1.33  
    1.34  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.35 -val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;
    1.36 +val PblObj {probl,...} = get_obj I pt [5];
    1.37 +    (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
    1.38  (*[
    1.39  (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
    1.40  (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),