1.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Tue Mar 31 14:05:10 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Tue Mar 31 15:43:33 2020 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4    val get_ctxt : ctree -> pos' -> Proof.context (*DEPRECATED*)
     1.5    val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
     1.6    val get_curr_formula : state -> term
     1.7 -  val get_assumptions_ : ctree -> pos' -> term list                             (* for appl.sml *)
     1.8 +  val get_assumptions : ctree -> pos' -> term list                             (* for appl.sml *)
     1.9  
    1.10    val new_val : term -> Istate_Def.T -> Istate_Def.T
    1.11    (* for calchead.sml *)
    1.12 @@ -100,7 +100,6 @@
    1.13    val g_res : ppobj -> term
    1.14    val g_res' : ctree -> term 
    1.15  (*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------
    1.16 -  val lev_on : CTbasic.pos -> CTbasic.pos                        (* duplicate in ctree-navi.sml *)
    1.17    val lev_dn : CTbasic.pos -> CTbasic.pos                        (* duplicate in ctree-navi.sml *)
    1.18    val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos   (* duplicate in ctree-navi.sml *)
    1.19     ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
    1.20 @@ -375,10 +374,6 @@
    1.21    | children _ = error "children: uncovered fun def.";
    1.22  
    1.23  (*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*)
    1.24 -fun lev_on [] = raise PTREE "lev_on []"
    1.25 -  | lev_on pos = 
    1.26 -    let val len = length pos
    1.27 -    in (drop_last pos) @ [(nth len pos)+1] end;
    1.28  fun lev_up [] = raise PTREE "lev_up []"
    1.29    | lev_up p = (drop_last p):pos;
    1.30  (* find the position of the next parent which is a PblObj in ctree *)
    1.31 @@ -488,7 +483,7 @@
    1.32    then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
    1.33    else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
    1.34  
    1.35 -fun get_assumptions_ pt p = get_ctxt pt p |> ContextC.get_assumptions;
    1.36 +fun get_assumptions pt p = get_ctxt pt p |> ContextC.get_assumptions;
    1.37  
    1.38  fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
    1.39    let