1.1 --- a/src/Tools/isac/Frontend/interface.sml	Thu Mar 15 15:48:52 2018 +0100
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Fri Mar 23 10:14:39 2018 +0100
     1.3 @@ -563,7 +563,7 @@
     1.4  (*.initContext Thy_ is conceptually impossible at [Pbl,Met]
     1.5     and at positions with Check_Postcond and End_Trans;
     1.6     at possible pos's there can be NO rewrite (returned as a context, too).*)
     1.7 -fun initContext cI Thy_ (pos as (p, p_):pos') =
     1.8 +fun initContext cI Celem.Thy_ (pos as (p, p_):pos') =
     1.9      ((if member op = [Pbl, Met] p_
    1.10        then message2xml cI "thy-context not to calchead"
    1.11        else if pos = ([], Res) then message2xml cI "no thy-context at result"
    1.12 @@ -601,7 +601,7 @@
    1.13        val chd = Math_Engine.initcontext_pbl pt (pp,p_)
    1.14      in contextpblOK2xml cI chd end)
    1.15        handle _ => sysERROR2xml cI "error in kernel 32")
    1.16 -  | initContext cI Met_ (p, p_) =
    1.17 +  | initContext cI Celem.Met_ (p, p_) =
    1.18      ((let
    1.19        val ((pt,_),_) = get_calc cI
    1.20        val pp = par_pblobj pt p