1.1 --- a/src/sml/ME/ctree.sml	Thu Feb 10 16:16:09 2005 +0100
     1.2 +++ b/src/sml/ME/ctree.sml	Thu Feb 10 17:13:10 2005 +0100
     1.3 @@ -1165,6 +1165,9 @@
     1.4    in if cut andalso length pos > 1 then cut_tree pt' (lev_up pos)
     1.5       else pt' end;
     1.6  *)
     1.7 +fun is_pblobj' pt (p:pos) =
     1.8 +    let val ppobj = get_obj I pt p
     1.9 +    in is_pblobj ppobj end;
    1.10  
    1.11  (*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
    1.12  fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =

     2.1 --- a/src/sml/ME/modspec.sml	Thu Feb 10 16:16:09 2005 +0100
     2.2 +++ b/src/sml/ME/modspec.sml	Thu Feb 10 17:13:10 2005 +0100
     2.3 @@ -1738,7 +1738,7 @@
     2.4  	   None => Form (pblterm dI pI)
     2.5  	 | Some t => Form (subst_atomic (mk_env probl) t)
     2.6      end;
     2.7 -(*vvv takes the tac generating the formula=result, asm ok....
     2.8 +(*vvv takes the tac _generating_ the formula=result, asm ok....
     2.9  fun pt_result (PrfObj {result=(t,asm), tac,...}) = 
    2.10      (Form t, 
    2.11       if null asm then None else Some asm, 
    2.12 @@ -1757,16 +1757,41 @@
    2.13  fun fst_onlev (([], Frm):pos') = true
    2.14    | fst_onlev (pos, Frm) = last_elem pos = 1
    2.15    | fst_onlev _ = false;
    2.16 +fun last_onlev pt pos = not (existpt (lev_on pos) pt);
    2.17  
    2.18 -
    2.19 +(*.pt_extract returns
    2.20 +      # the formula at pos
    2.21 +      # the tactic applied to this formula
    2.22 +      # the list of assumptions generated at this formula
    2.23 +	(by application of another tac to the preceding formula !)
    2.24 +   pos is assumed to come from the frontend, ie. generated by moveDown.*)
    2.25  (*cannot be in ctree.sml, because ModSpec has to be calculated;
    2.26    TODO.WN040107: check if !applied! (NOT generating) tac is returned *)
    2.27  (* val pos as (p,p_) = ([1],Res);
    2.28     val pos as (p,p_) = ([2],Frm);
    2.29     *)
    2.30 -fun pt_extract (pt,(p,Res)) =
    2.31 +fun pt_extract (pt,([],Res)) =
    2.32 +    let val (f, asm) = get_obj g_result pt []
    2.33 +    in (Form f, None, asm) end
    2.34 +
    2.35 +  | pt_extract (pt,(p,Res)) =
    2.36      let val (f, asm) = get_obj g_result pt p
    2.37 -    in (Form f, Some Empty_Tac, asm) end
    2.38 +	val tac = Empty_Tac
    2.39 +(*
    2.40 +	val tac = if last_onlev pt p
    2.41 +		  then if is_pblobj' pt p
    2.42 +		       then let val (PblObj{spec=(_,pI,_),...})= get_obj I pt p
    2.43 +			    in if pI = e_pblID then None 
    2.44 +			       else Some (Check_Postcond pI) end
    2.45 +		       else Some End_Trans
    2.46 +		  else 
    2.47 +
    2.48 +
    2.49 +@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
    2.50 +
    2.51 +
    2.52 +*)
    2.53 +    in (Form f, Some tac, asm) end
    2.54  
    2.55    | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
    2.56  (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
    2.57 @@ -1774,10 +1799,7 @@
    2.58      let val ppobj = get_obj I pt p
    2.59  	val f = if is_pblobj ppobj then pt_model ppobj p_
    2.60  		else get_obj pt_form pt p
    2.61 -	val (_, asm) = if fst_onlev pos orelse null p
    2.62 -			 then (e_term, [])
    2.63 -			 else get_obj g_result pt (lev_pred p) (*#!#*)
    2.64 -    in (f, Some Empty_Tac, asm) end;
    2.65 +    in (f, Some Empty_Tac, []) end;
    2.66  
    2.67  
    2.68  (**. get the formula from a ctree-node:

     3.1 --- a/src/sml/ROOT.ML	Thu Feb 10 16:16:09 2005 +0100
     3.2 +++ b/src/sml/ROOT.ML	Thu Feb 10 17:13:10 2005 +0100
     3.3 @@ -75,7 +75,7 @@
     3.4  
     3.5  *)
     3.6  
     3.7 -  val version_kernel = "sml-050210a-before-asms";
     3.8 +  val version_kernel = "sml-050210b";
     3.9  
    3.10    print_depth 3; 
    3.11