test/Tools/isac/Minisubpbl/300-init-subpbl.sml
changeset 59881 bdced24f62bf
parent 59846 7184a26ac7d5
child 59898 68883c046963
     1.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Wed Apr 15 16:46:41 2020 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Wed Apr 15 18:00:58 2020 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4    Generate.generate1 tac (istate, ctxt) (pt, (p', p_));
     1.5  "~~~~~ fun generate1 , args:"; val (thy, (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)),
     1.6        (l as (_, ctxt)), (pos as (p, p_)), pt)
     1.7 -  = ((Celem.assoc_thy "Isac_Knowledge"), tac, (istate, ctxt), (p', p_), pt);
     1.8 +  = ((ThyC.get_theory "Isac_Knowledge"), tac, (istate, ctxt), (p', p_), pt);
     1.9  	    val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
    1.10  	      (oris, (domID, pblID, metID), hdl, ctxt_specify);
    1.11