1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Jul 24 08:09:06 2015 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Fri Aug 07 15:52:17 2015 +0200
     1.3 @@ -68,6 +68,9 @@
     1.4  
     1.5  section {*check presence of definitions from directories*}
     1.6  
     1.7 +ML {*
     1.8 +*} ML {*
     1.9 +*}
    1.10  ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
    1.11  ML {* me; (*from "Interpret/mathengine.sml"*) *}
    1.12  ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}

     2.1 --- a/src/Tools/isac/Frontend/interface.sml	Fri Jul 24 08:09:06 2015 +0200
     2.2 +++ b/src/Tools/isac/Frontend/interface.sml	Fri Aug 07 15:52:17 2015 +0200
     2.3 @@ -282,16 +282,16 @@
     2.4       getasmsOK2xml cI ass end)
     2.5      handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
     2.6  
     2.7 -
     2.8  (*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
     2.9    refFormula might become involved in far-off errors !!!*)
    2.10 -fun refFormula cI (p:pos') = (*WN0501 rename to 'fun getElement' !*)
    2.11 -(* val (cI, uI) = (1,1);
    2.12 -   *)
    2.13 -    (let val ((pt,_),_) = get_calc cI
    2.14 -	 val (form, tac, asms) = pt_extract (pt, p)
    2.15 -    in refformulaOK2xml cI p form end)
    2.16 -    handle _ => sysERROR2xml cI "error in kernel 6";
    2.17 +fun refFormula cI (p: pos') = (*WN0501 rename to 'fun getElement' !*)
    2.18 +  (let 
    2.19 +    val ((pt, _), _) = get_calc cI
    2.20 +	  val (form, _, _) = pt_extract (pt, p)
    2.21 +  in refformulaOK2xml cI p form end)
    2.22 +    handle _ => 
    2.23 +      sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ 
    2.24 +        " " ^ pos'2str p);
    2.25  
    2.26  (*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p);
    2.27     in case of CalcHeads only the headline is taken

     3.1 --- a/src/Tools/isac/Interpret/ctree.sml	Fri Jul 24 08:09:06 2015 +0200
     3.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Fri Aug 07 15:52:17 2015 +0200
     3.3 @@ -1215,14 +1215,10 @@
     3.4       spec;                 (*specification*)
     3.5  val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
     3.6  
     3.7 -datatype ptform =
     3.8 -	 Form of term
     3.9 -       | ModSpec of ocalhd;
    3.10 +datatype ptform = Form of term | ModSpec of ocalhd;
    3.11  val e_ptform = Form e_term;
    3.12  val e_ptform' = ModSpec e_ocalhd;
    3.13  
    3.14 -
    3.15 -
    3.16  (*.applies (snd f) to the branches at a pos if ((fst f) b),
    3.17     f : (ppobj -> bool) * (int -> ptree list -> ptree list).*)
    3.18