(* Title:  Specify-phase: specifying and modeling a problem or a subproblem. The

            most important types are declared in mstools.sml.

    Author: Walther Neuper 991122, Mathias Lehnfeld

    (c) due to copyright terms

 *)

 signature CALC_HEAD =

 sig

   type calcstate

   type calcstate'

   datatype appl = Appl of tac_ | Notappl of string

   val nxt_specify_init_calc : fmz -> calcstate

   val specify : tac_ -> pos' -> cid -> ptree ->

     (posel list * pos_) * ((posel list * pos_) * istate) * Ctree.mout * tac * safe * ptree

   val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'

   val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->

     (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac

   val reset_calchead : ptree * pos' -> ptree * pos'

   val get_ocalhd : ptree * pos' -> ocalhd

   val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool

   val all_modspec : ptree * pos' -> ptree * pos' 

   val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list

   val insert_ppc' : itm -> itm list -> itm list

   val complete_mod : ptree * pos' -> ptree * pos'

   val is_complete_mod : ptree * pos' -> bool

   val complete_spec : ptree * pos' -> ptree * pos' 

   val is_complete_spec : ptree * pos' -> bool

   val some_spec : spec -> spec -> spec

   (* these could go to Ctree ..*)

   val show_pt : ptree -> unit

   val pt_extract : ptree * (posel list * pos_) -> ptform * tac option * term list 

   val get_interval : int list * pos_ -> pos' -> int -> ptree -> (pos' * term) list

   val match_ags : theory -> pat list -> term list -> ori list

   val match_ags_msg : pblID -> term -> term list -> unit

   val oris2fmz_vals : ori list -> string list * term list

   val vars_of_pbl_' : ('a * ('b * term)) list -> term list

   val is_known : Proof.context -> string -> ori list -> term -> string * ori * term list

   val is_notyet_input : Proof.context -> itm list -> term list -> ori -> ('a * (term * term)) list

     -> string * itm

   val e_calcstate' : calcstate'

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   val vals_of_oris : ori list -> term list

   val is_error : itm_ -> bool

   val is_copy_named : 'a * ('b * term) -> bool

   val ori2Coritm : pat list -> ori -> itm

   val ppc2list : 'a ppc -> 'a list

   val is_copy_named_idstr : string -> bool

   val matc : theory -> (string * (term * term)) list -> term list -> preori list -> preori list

   val mtc : theory -> pat -> term -> preori option

   val cpy_nam : pat list -> preori list -> pat -> preori

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 structure Chead(**): CALC_HEAD(**) =

 struct

 (* datatypes *)

 (* the state wich is stored after each step of calculation; it contains

    the calc-state and a list of [tac,istate](="tacis") to be applied next.

    the last_elem tacis is the first to apply to the calc-state and

    the (only) one shown to the front-end as the 'proposed tac'.

    the calc-state resulting from the application of tacis is not stored,

    because the tacis hold enough information for efficiently rebuilding

    this state just by "fun generate "

 *)

 type calcstate = 

   (ptree * pos') *    (* the calc-state to which the tacis could be applied *)

   (Ctree.taci list)   (* ev. several (hidden) steps; 

                          in REVERSE order: first tac_ to apply is last_elem *)

 val e_calcstate = ((EmptyPtree, e_pos'), [Ctree.e_taci]) : calcstate;

 (*the state used during one calculation within the mathengine; it contains

   a list of [tac,istate](="tacis") which generated the the calc-state;

   while this state's tacis are extended by each (internal) step,

   the calc-state is used for creating new nodes in the calc-tree

   (eg. applicable_in requires several particular nodes of the calc-tree)

   and then replaced by the the newly created;

   on leave of the mathengine the resuing calc-state is dropped anyway,

   because the tacis hold enought information for efficiently rebuilding

   this state just by "fun generate ".*)

 type calcstate' = 

   Ctree.taci list * (* cas. several (hidden) steps;

                        in REVERSE order: first tac_ to apply is last_elem                   *)

   pos' list *       (* a "continuous" sequence of pos', deleted by application of taci list *)     

   (ptree * pos')    (* the calc-state resulting from the application of tacis               *)

 val e_calcstate' = ([Ctree.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';

 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)

 fun f_mout thy (Ctree.Form' (Ctree.FormKF (_, _, _, _, f))) = (Thm.term_of o the o (parse thy)) f

   | f_mout _ _ = error "f_mout: not called with formula";

 (* is the calchead complete ? *)

 fun ocalhd_complete its pre (dI, pI, mI) = 

   foldl and_ (true, map #3 its) andalso 

   foldl and_ (true, map #1 pre) andalso 

   dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID

 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris 

    --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)

 fun oris2fmz_vals oris =

   let fun ori2fmz_vals ((_, _, _, dsc, ts): ori) = 

 	  ((term2str o comp_dts') (dsc, ts), last_elem ts) 

 	  handle _ => error ("ori2fmz_env called with " ^ terms2str ts)

   in (split_list o (map ori2fmz_vals)) oris end

 (* make a term 'typeless' for comparing with another 'typeless' term;

    'type-less' usually is illtyped                                  *)

 fun typeless (Const (s, _)) = (Const (s, e_type)) 

   | typeless (Free (s, _)) = (Free (s, e_type))

   | typeless (Var (n, _)) = (Var (n, e_type))

   | typeless (Bound i) = (Bound i)

   | typeless (Abs (s, _,t)) = Abs(s, e_type, typeless t)

   | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)

 (* to an input (d,ts) find the according ori and insert the ts)

   WN.11.03: + dont take first inter<>[]                       *)

 fun seek_oridts ctxt sel (d, ts) [] =

     ("seek_oridts: input ('" ^

         (term_to_string' ctxt (comp_dts (d, ts))) ^ "') not found in oris (typed)",

       (0, [], sel, d, ts),

       [])

   | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =

     if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []

     then ("", (id, vat, sel, d, inter op = ts ts'), ts')

     else seek_oridts ctxt sel (d, ts) oris

 (* to an input (_,ts) find the according ori and insert the ts *)

 fun seek_orits ctxt _ ts [] = 

     ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^

     "') not found in oris (typed)", e_ori_, [])

   | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: (oris: ori list)) =

     if sel = sel' andalso (inter op = ts ts') <> [] 

     then

       if sel = sel' 

       then ("", (id, vat, sel, d, inter op = ts ts'): ori, ts')

       else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])

     else seek_orits ctxt sel ts oris

 (* find_first item with #1 equal to id *)

 fun seek_ppc _ [] = NONE

   | seek_ppc id (p :: (ppc: itm list)) = if id = #1 p then SOME p else seek_ppc id ppc

 datatype appl =

   Appl of tac_      (* tactic is applicable at a certain position in the Ctree *)

 | Notappl of string (* tactic is NOT applicable                                *)

 fun ppc2list ({Given = gis, Where = whs, Find = fis, With = wis, Relate = res}: 'a ppc) =

   gis @ whs @ fis @ wis @ res

 fun ppc135list ({Given = gis, Find = fis, Relate = res, ...}: 'a ppc) = gis @ fis @ res

 (* get the number of variants in a problem in 'original',

    assumes equal descriptions in immediate sequence    *)

 fun variants_in ts =

   let

     fun eq (x, y) = head_of x = head_of y

     fun cnt _ [] _ n = ([n], [])

       | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)

     fun coll _  xs [] = xs

       | coll eq  xs (y :: ys) = 

         let val (n, ys') = cnt eq (y :: ys) y 0

         in if ys' = [] then xs @ n else coll eq  (xs @ n) ys' end

     val vts = subtract op = [1] (distinct (coll eq [] ts))

   in

     case vts of 

       [] => 1

     | [n] => n

     | _ => error "different variants in formalization"

   end

 fun is_list_type (Type ("List.list", _)) = true

   | is_list_type _ = false

 fun has_list_type (Free (_, T)) = is_list_type T

   | has_list_type _ = false

 fun is_parsed (Syn _) = false

   | is_parsed _ = true

 fun parse_ok its = foldl and_ (true, map is_parsed its)

 fun all_dsc_in itm_s =

   let    

     fun d_in (Cor ((d, _), _)) = [d]

       | d_in (Syn _) = []

       | d_in (Typ _) = []

       | d_in (Inc ((d,_),_)) = [d]

       | d_in (Sup (d,_)) = [d]

       | d_in (Mis (d,_)) = [d]

       | d_in i = error ("all_dsc_in: uncovered case with " ^ itm_2str i)

   in (flat o (map d_in)) itm_s end; 

 fun is_error (Cor _) = false

   | is_error (Sup _) = false

   | is_error (Inc _) = false

   | is_error (Mis _) = false

   | is_error _ = true

 (* get the first term in ts from ori *)

 fun getr_ct thy ((_, _, fd, d, ts) : ori) =

   (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm')

 (* get a term from ori, notyet input in itm.

    the term from ori is thrown back to a string in order to reuse

    machinery for immediate input by the user. *)

 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =

   (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')

 (* in FE dsc, not dat: this is in itms ...*)

 fun is_untouched ((_, _, false, _, Inc ((_, []), _)): itm) = true

   | is_untouched _ = false

 (* select an item in oris, notyet input in itms 

    (precondition: in itms are only Cor, Sup, Inc) *)

 (*args of nxt_add

   thy : for?

   oris: from formalization 'type fmz', structured for efficient access 

   pbt : the problem-pattern to be matched with oris in order to get itms

   itms: already input items

 *)

 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)

     let

       fun test_d d ((i, _, _, _, itm_): itm) = (d = (d_in itm_)) andalso i <> 0

       fun is_elem itms (_, (d, _)) = 

         case find_first (test_d d) itms of SOME _ => true | NONE => false

     in

       case filter_out (is_elem itms) pbt of

         (f, (d, _)) :: _ => SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')

       | _ => NONE

     end

   | nxt_add thy oris _ itms =

     let

       fun testr_vt v ori = member op= (#2 (ori:ori)) v andalso (#3 ori) <> "#undef"

       fun testi_vt v itm =member op= (#2 (itm:itm)) v

       fun test_id ids r = member op= ids (#1 (r:ori))

       fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = 

         (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts)

       fun false_and_not_Sup ((_, _, false, _, Sup _): itm) = false

         | false_and_not_Sup (_, _, false, _, _) = true

         | false_and_not_Sup _ = false

       val v = if itms = [] then 1 else max_vt itms

       val vors = if v = 0 then oris else filter (testr_vt v) oris  (* oris..vat *)

       val vits =

         if v = 0

         then itms                                 (* because of dsc without dat *)

   	    else filter (testi_vt v) itms;                             (* itms..vat *)

       val icl = filter false_and_not_Sup vits;                    (* incomplete *)

     in

       if icl = [] 

       then case filter_out (test_id (map #1 vits)) vors of

   	    [] => NONE

   	  | miss => SOME (getr_ct thy (hd miss))

       else

         case find_first (test_subset (hd icl)) vors of

           NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"

         | SOME ori => SOME (geti_ct thy ori (hd icl))

     end

 fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)

   | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)

   | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)

   | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")

 fun mk_additem "#Given" ct = Add_Given ct

   | mk_additem "#Find" ct = Add_Find ct    

   | mk_additem "#Relate"ct = Add_Relation ct

   | mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"")

 (* determine the next step of specification;

    not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))

    eg. in rootpbl 'no_met': 

 args:

   preok          predicates are _all_ ok (and problem matches completely)

   oris           immediately from formalization 

   (dI',pI',mI')  specification coming from author/parent-problem

   (pbl,          item lists specified by user

    met)          -"-, tacitly completed by copy_probl

   (dI,pI,mI)     specification explicitly done by the user

   (pbt, mpc)     problem type, guard of method

 *)

 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)

       ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) = 

     (if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')

      else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')

      else

        case find_first (is_error o #5) (pbl:itm list) of

 	       SOME (_, _, _, fd, itm_) =>

 	         (Pbl, mk_delete (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)

 	     | NONE => 

 	       (case nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl of

 	          SOME (fd,ct') => (Pbl, mk_additem fd ct')

 	        | NONE => (*pbl-items complete*)

 	          if not preok then (Pbl, Refine_Problem pI')

 	          else if dI = e_domID then (Pbl, Specify_Theory dI')

 		        else if pI = e_pblID then (Pbl, Specify_Problem pI')

 		        else if mI = e_metID then (Pbl, Specify_Method mI')

 		        else

 			        case find_first (is_error o #5) met of

 			          SOME (_, _, _, fd, itm_) => (Met, mk_delete (assoc_thy dI) fd itm_)

 			        | NONE => 

 			          (case nxt_add (assoc_thy dI) oris mpc met of

 				          SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)

 				        | NONE => (Met, Apply_Method mI))))

   | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) = 

     (case find_first (is_error o #5) met of

       SOME (_,_,_,fd,itm_) => (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)

     | NONE => 

       case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of

 	      SOME (fd,ct') => (Met, mk_additem fd ct')

       | NONE => 

 	      (if dI = e_domID then (Met, Specify_Theory dI')

 	       else if pI = e_pblID then (Met, Specify_Problem pI')

 		     else if not preok then (Met, Specify_Method mI)

 		     else (Met, Apply_Method mI)))

   | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)

 fun is_field_correct sel d dscpbt =

   case assoc (dscpbt, sel) of

     NONE => false

   | SOME ds => member op = ds d

 (* update the itm_ already input, all..from ori *)

 fun ori_2itm itm_ pid all ((id, vt, fd, d, ts): ori) = 

   let 

     val ts' = union op = (ts_in itm_) ts;

     val pval = pbl_ids' d ts'

 	  (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)

     val complete = if eq_set op = (ts', all) then true else false

   in

     case itm_ of

       (Cor _) => 

         (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts')) 

 	       else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval)))): itm

     | (Syn c) => error ("ori_2itm wants to overwrite " ^ c)

     | (Typ c) => error ("ori_2itm wants to overwrite " ^ c)

     | (Inc _) =>

       if complete

   	  then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))

   	  else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))

     | (Sup (d,ts')) => (*4.9.01 lost env*)

   	  (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))

   	  (*else (id,vt,complete,fd,Cor((d,ts'),e))*)

       (* 28.1.00: not completely clear ---^^^ etc.*)

     | (Mis _) => (* 4.9.01: Mis just copied *)

        if complete

   		 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))

   		 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))

     | i => error ("ori_2itm: uncovered case of "^ itm_2str i)

   end

 fun eq1 d (_, (d', _)) = (d = d')

 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_) 

 (* 'all' ts from ori; ts is the input; (ori carries rest of info)

    9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?

    pval: value for problem-environment _NOT_ checked for 'inter' --

    -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc

   (as it has been done for input_icalhd+insert_ppc' in 11.03)*)

 (*. is_input ori itms <=> 

     EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)

             (2) ori(ts) subset itm(ts)        --- Err "already input"       

 	    (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)

 	    (4) -"- <> empty                  --- new: ori(ts) \\ inter .*)

 fun is_notyet_input ctxt (itms: itm list) all ((i, v, f, d, ts): ori) pbt =

   case find_first (eq1 d) pbt of

     SOME (_, (_, pid)) =>

       (case find_first (eq3 f d) itms of

         SOME (_,_,_,_,itm_) =>

           let val ts' = inter op = (ts_in itm_) ts

           in 

             if subset op = (ts, ts') 

             then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm) (*2*)

 	          else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts))              (*3,4*)

 	          end

 	    | NONE => ("", ori_2itm (Inc ((e_term, []), (pid, []))) pid all (i, v, f, d, ts)))    (*1*)

   | NONE => ("", ori_2itm (Sup (d, ts)) e_term all (i, v, f, d, ts))

 fun test_types ctxt (d,ts) =

   let 

     val opt = (try comp_dts) (d, ts)

     val msg = case opt of 

       SOME _ => "" 

     | NONE => (term_to_string' ctxt d ^ " " ^

 	    (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped")

   in msg end

 (* is the input term t known in oris ? 

    give feedback on all(?) strange input;

    return _all_ terms already input to this item (e.g. valuesFor a,b) *)

 fun is_known ctxt sel ori t =

   let

     val _ = tracing ("RM is_known: t=" ^ term2str t)

     val ots = (distinct o flat o (map #5)) (ori:ori list)

     val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots

     val (d, ts) = split_dts t

     val ids = map (fst o dest_Free) ((distinct o (flat o (map vars))) ts)

   in

     if (subtract op = oids ids) <> []

     then (("identifiers "^(strs2str' (subtract op = oids ids)) ^ " not in example"), e_ori_, [])

     else 

 	    if d = e_term 

 	    then 

 	      if not (subset op = (map typeless ts, map typeless ots))

 	      then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^

 		      "' not in example (typeless)", e_ori_, [])

 	      else 

           (case seek_orits ctxt sel ts ori of

 		         ("", ori_ as (_,_,_,d,ts), all) =>

 		            (case test_types ctxt (d,ts) of

 		              "" => ("", ori_, all)

 		            | msg => (msg, e_ori_, []))

 		       | (msg,_,_) => (msg, e_ori_, []))

 	    else 

 	      if member op = (map #4 ori) d

 	      then seek_oridts ctxt sel (d, ts) ori

 	      else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])

   end

 datatype additm =

 	 Add of itm   (* return-value of appl_add *)

 | Err of string (* error-message            *)

 (* add an item to the model; check wrt. oris and pbt.

    in contrary to oris<>[] below, this part handles user-input

    extremely acceptive, i.e. accept input instead error-msg  *)

 fun appl_add ctxt sel [] ppc pbt ct =

     let

       val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)

       in 

         case parseNEW ctxt ct of

           NONE => Add (i, [], false, sel, Syn ct)

         | SOME t =>

             let val (d, ts) = split_dts t

             in 

               if d = e_term 

               then Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) 

               else

                 (case find_first (eq1 d) pbt of

                    NONE => Add (i, [], true, sel, Sup (d,ts))

                  | SOME (f, (_, id)) =>

                      let fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0

                      in case find_first (eq2 d) ppc of

                        NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))

                      | SOME (i', _, _, _, itm_) => 

                          if is_list_dsc d 

                          then 

                            let

                              val in_itm = ts_in itm_

                              val ts' = union op = ts in_itm

                              val i'' = if in_itm = [] then i else i'

                            in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end

                          else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))

                      end)

             end

     end

   | appl_add ctxt sel oris ppc pbt str =

     case parseNEW ctxt str of

       NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")

     | SOME t => 

         case is_known ctxt sel oris t of

           ("", ori', all) => 

             (case is_notyet_input ctxt ppc all ori' pbt of

                ("", itm) => Add itm

              | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))

         | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);

 (* make oris from args of the stac SubProblem and from pbt.

    can this formal argument (of a model-pattern) be omitted in the arg-list

    of a SubProblem ? see calcelems.sml 'type met '                        *)

 fun is_copy_named_idstr str =

   case (rev o Symbol.explode) str of

 	  "'" :: _ :: "'" :: _ =>

 	  (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " T"); true)

   | _ =>

     (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " F"); false)

 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t

 (* should this formal argument (of a model-pattern) create a new identifier? *)

 fun is_copy_named_generating_idstr str =

   if is_copy_named_idstr str

   then

     case (rev o Symbol.explode) str of

 	    "'" :: "'" :: "'" :: _ => false

     | _ => true

   else false

 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o free2str) t

 (* split type-wrapper from scr-arg and build part of an ori;

    an type-error is reported immediately, raises an exn, 

    subsequent handling of exn provides 2nd part of error message *)

 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =

     ((Thm.global_cterm_of thy (dsc $ var);(*type check*)

       SOME ((([1], str, dsc, (*[var]*)

 	    split_dts' (dsc, var))): preori)(*:ori without leading #*))

       handle e as TYPE _ => 

 	      (tracing (dashs 70 ^ "\n"

 	        ^ "*** ERROR while creating the items for the model of the ->problem\n"

 	        ^ "*** from the ->stac with ->typeconstructor in arglist:\n"

 	        ^ "*** item (->description ->value): " ^ term2str dsc ^ " " ^ term2str var ^ "\n"

 	        ^ "*** description: " ^ term_detail2str dsc

 	        ^ "*** value: " ^ term_detail2str var

 	        ^ "*** typeconstructor in script: " ^ term_detail2str ty

 	        ^ "*** checked by theory: " ^ theory2str thy ^ "\n"

 	        ^ "*** " ^ dots 66);

           writeln (PolyML.makestring e);

           reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)

       NONE))

   | mtc _ _ t = error ("mtc: uncovered case with" ^ term2str t)

 (* match each pat of the model-pattern with an actual argument;

    precondition: copy-named vars are filtered out            *)

 fun matc _ ([]:pat list)  _  (oris:preori list) = oris

   | matc _ pbt [] _ =

     (tracing (dashs 70);

      error ("actual arg(s) missing for '" ^ pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))

   | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =

     (*del?..*)if (is_copy_named_idstr o free2str) t then oris

     else(*..del?*)

       let val opt = mtc thy p a

       in

         case opt of

           SOME ori => matc thy pbt ags (oris @ [ori])

 	      | NONE => [](*WN050903 skipped by exn handled in match_ags*)

 	 end

 (* generate a new variable "x_i" name from a related given one "x"

    by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"

    e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),

    but leave is_copy_named_generating as is, e.t. ss''' *)

 fun cpy_nam (pbt: pat list) (oris: preori list) (p as (field, (dsc, t)): pat) =

   (if is_copy_named_generating p

    then (*WN051014 kept strange old code ...*)

      let fun sel (_,_,d,ts) = comp_ts (d, ts) 

        val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t

        val ext = (last_elem o drop_last o Symbol.explode o free2str) t

        val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)

        val vals = map sel oris

        val cy_ext = (free2str o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext

      in ([1], field, dsc, [mk_free (type_of t) cy_ext]): preori end

    else ([1], field, dsc, [t])

 	) handle _ => error ("cpy_nam: for "^(term2str t))

 (* match the actual arguments of a SubProblem with a model-pattern

    and create an ori list (in root-pbl created from formalization).

    expects ags:pats = 1:1, while copy-named are filtered out of pats;

    if no 1:1 the exn raised by matc/mtc and handled at call.

    copy-named pats are appended in order to get them into the model-items *)

 fun match_ags thy (pbt: pat list) ags =

   let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_)

     val pbt' = filter_out is_copy_named pbt

     val cy = filter is_copy_named pbt

     val oris' = matc thy pbt' ags []

     val cy' = map (cpy_nam pbt' oris') cy

     val ors = add_id (oris' @ cy') (*...appended in order to get into the model-items *)

   in (map flattup ors): ori list end

 (* report part of the error-msg which is not available in match_args *)

 fun match_ags_msg pI stac ags =

   let

     val pats = (#ppc o get_pbt) pI

     val msg = (dots 70^"\n"

        ^ "*** problem "^strs2str pI ^ " has the ...\n"

        ^ "*** model-pattern "^pats2str pats ^ "\n"

        ^ "*** stac   '"^term2str stac ^ "' has the ...\n"

        ^ "*** arg-list "^terms2str ags ^ "\n"

        ^ dashs 70)

 	  (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)

   in tracing msg end

 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)

 fun vars_of_pbl_ pbl_ = 

   let

     fun var_of_pbl_ (_, (_, t)) = t

   in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end

 fun vars_of_pbl_' pbl_ = 

   let

     fun var_of_pbl_ (_, (_, t)) = t: term

   in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end

 fun overwrite_ppc thy itm ppc =

   let 

     fun repl _ (_, _, _, _, itm_) [] =

         error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ " not found")

       | repl ppc' itm (p :: ppc) =

 	      if (#1 itm) = (#1 (p: itm))

 	      then ppc' @ [itm] @ ppc

 	      else repl (ppc' @ [p]) itm ppc

   in repl [] itm ppc end

 (* 10.3.00: insert the already compiled itm into model;

    ev. filter_out  untouched (in FE: (0,...)) item related to insert-item *)

 fun insert_ppc thy itm ppc =

   let 

     fun eq_untouched d ((0, _, _, _, itm_): itm) = (d = d_in itm_)

       | eq_untouched _ _ = false

     val ppc' = case seek_ppc (#1 itm) ppc of

       SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)

     | NONE => (ppc @ [itm])

   in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end

 fun eq_dsc ((_, _, _, _, itm_): itm, (_, _, _, _, iitm_): itm) = (d_in itm_ = d_in iitm_)

 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,

    handles superfluous items carelessly                       *)

 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)

 (* output the headline to a ppc *)

 fun header p_ pI mI =

   case p_ of Pbl => Ctree.Problem (if pI = e_pblID then [] else pI) 

 	   | Met => Ctree.Method mI

 	   | pos => error ("header called with "^ pos_2str pos)

 fun specify_additem sel (ct, _) (p, Met) _ pt = 

     let

       val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of

         (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})

           => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)

   	  | _ => error "specify_additem: uncovered case of get_obj I pt p"

       val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI

       val cpI = if pI = e_pblID then pI' else pI

       val cmI = if mI = e_metID then mI' else mI

       val {ppc, pre, prls, ...} = get_met cmI

     in 

       case appl_add ctxt sel oris met ppc ct of

         Add itm =>  (*..union old input *)

   	      let

             val met' = insert_ppc thy itm met

             val arg = case sel of

   			      "#Given" => Add_Given'   (ct, met')

   		      | "#Find"  => Add_Find'    (ct, met')

   		      | "#Relate"=> Add_Relation'(ct, met')

   		      | str => error ("specify_additem: uncovered case with " ^ str)

   	        val (p, Met, pt') = case Ctree.generate1 thy arg (Uistate, ctxt) (p, Met) pt of

   	          ((p, Met), _, _, pt') => (p, Met, pt')

   	        | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"

   	        val pre' = check_preconds thy prls pre met'

   	        val pb = foldl and_ (true, map fst pre')

   	        val (p_, nxt) =

   	          nxt_spec Met pb oris (dI',pI',mI') (pbl,met') 

   	            ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);

   	      in ((p, p_), ((p, p_), Uistate),

   	        Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef,

   		        (Ctree.Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')

           end

       | Err msg =>

   	      let

             val pre' = check_preconds thy prls pre met

   	        val pb = foldl and_ (true, map fst pre')

   	        val (p_, nxt) =

   	          nxt_spec Met pb oris (dI',pI',mI') (pbl,met) 

   	            ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);

   	      in ((p,p_), ((p,p_),Uistate), Ctree.Error' (Ctree.Error_ msg), nxt, Safe,pt) end

     end

   | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt = 

       let

         val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of

           (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})

             => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)

   	    | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"

         val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI

         val cpI = if pI = e_pblID then pI' else pI

         val cmI = if mI = e_metID then mI' else mI

         val {ppc, where_, prls, ...} = get_pbt cpI

       in

         case appl_add ctxt sel oris pbl ppc ct of

           Add itm => (*..union old input *)

 	          let

 	            val pbl' = insert_ppc thy itm pbl

               val arg = case sel of

   			        "#Given" => Add_Given'   (ct, pbl')

   		        | "#Find"  => Add_Find'    (ct, pbl')

   		        | "#Relate"=> Add_Relation'(ct, pbl')

   		        | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)

 	            val ((p, Pbl), _, _, pt') = Ctree.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)

 	            val pre = check_preconds thy prls where_ pbl'

 	            val pb = foldl and_ (true, map fst pre)

 	            val (p_, nxt) =

 	              nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)

 	            val ppc = if p_= Pbl then pbl' else met

 	          in

 	            ((p, p_), ((p, p_), Uistate),

 	            Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef,

 			          (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt, Safe, pt')

             end

         | Err msg =>

 	          let

               val pre = check_preconds thy prls where_ pbl

 	            val pb = foldl and_ (true, map fst pre)

 	            val (p_, nxt) =

 	              nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met) 

 	                (ppc, (#ppc o get_met) cmI) (dI, pI, mI)

 	          in ((p, p_), ((p, p_), Uistate), Ctree.Error' (Ctree.Error_ msg), nxt, Safe,pt) end

       end

 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ = 

     let          (* either """"""""""""""" all empty or complete *)

       val thy = assoc_thy dI'

       val (oris, ctxt) = 

         if dI' = e_domID orelse pI' = e_pblID  (*andalso? WN110511*)

         then ([], e_ctxt)

   	    else pI' |> #ppc o get_pbt |> prep_ori fmz thy

       val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec')

   			(oris, (dI',pI',mI'), e_term)

       val pt = update_ctxt pt [] ctxt

       val (pbl, pre) = ([], [])

     in 

       case mI' of

   	    ["no_met"] => 

   	      (([], Pbl), (([], Pbl), Uistate),

   	        Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length [], Ctree.Nundef, (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre))),

   	        Refine_Tacitly pI', Safe, pt)

        | _ => 

   	      (([], Pbl), (([], Pbl), Uistate),

   	        Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length [], Ctree.Nundef, (Ctree.Problem [], itms2itemppc (assoc_thy dI') pbl pre))),

   	        Model_Problem, Safe, pt)

     end

     (* ONLY for STARTING modeling phase *)

   | specify (Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =

     let 

       val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of

         PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>

           (oris, dI',pI',mI', dI, ctxt)

       | _ => error "specify (Model_Problem': uncovered case get_obj"

       val thy' = if dI = e_domID then dI' else dI

       val thy = assoc_thy thy'

       val {ppc, prls, where_, ...} = get_pbt pI'

       val pre = check_preconds thy prls where_ pbl

       val pb = foldl and_ (true, map fst pre)

       val ((p, _), _, _, pt) =

         Ctree.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt

       val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met) 

 		    (ppc,(#ppc o get_met) mI') (dI',pI',mI');

     in

       ((p, Pbl), ((p, p_), Uistate), 

       Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),

       nxt, Safe, pt)

     end

     (* called only if no_met is specified *)     

   | specify (Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =

       let

         val (dI', ctxt) = case get_obj I pt p of

           PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)

         | _ => error "specify (Refine_Tacitly': uncovered case get_obj"

         val {met, thy,...} = get_pbt pIre

         val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)

         val ((p,_), _, _, pt) = 

 	        Ctree.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt

         val (pbl, pre, _) = ([], [], false)

       in ((p, Pbl), (pos, Uistate),

         Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),

         Model_Problem, Safe, pt)

       end

   | specify (Refine_Problem' rfd) pos _ pt =

       let

         val ctxt = get_ctxt pt pos

         val (pos, _, _, pt) =

           Ctree.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt

       in

         (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Ctree.Problems (Ctree.RefinedKF rfd), Model_Problem, Safe, pt)

       end

     (*WN110515 initialise ctxt again from itms and add preconds*)

   | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =

       let

         val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of

           PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>

             (oris, dI', pI', mI', dI, mI, ctxt, met)

         | _ => error "specify (Specify_Problem': uncovered case get_obj"

         val thy = assoc_thy dI

         val (p, Pbl, pt) =

           case  Ctree.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of

             ((p, Pbl), _, _, pt) => (p, Pbl, pt)

           | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"

         val dI'' = assoc_thy (if dI=e_domID then dI' else dI)

         val mI'' = if mI=e_metID then mI' else mI

         val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o get_pbt) pI,

           (#ppc o get_met) mI'') (dI, pI, mI);

       in

         ((p,Pbl), (pos,Uistate),

         Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Problem pI, itms2itemppc dI'' itms pre))),

         nxt, Safe, pt)

       end    

     (*WN110515 initialise ctxt again from itms and add preconds*)

   | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) _ pt =

       let

         val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of

           PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>

              (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)

         | _ => error "specify (Specify_Problem': uncovered case get_obj"

         val {ppc,pre,prls,...} = get_met mID

         val thy = assoc_thy dI

         val oris = add_field' thy ppc oris

         val dI'' = if dI=e_domID then dI' else dI

         val pI'' = if pI = e_pblID then pI' else pI

         val met = if met = [] then pbl else met

         val (_, (itms, pre')) = match_itms_oris thy met (ppc, pre, prls ) oris

         val (pos, _, _, pt) = 

 	        Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt

         val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms) 

 		      ((#ppc o get_pbt) pI'', ppc) (dI'', pI'', mID)

       in

         (pos, (pos,Uistate),

         Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (Ctree.Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),

         nxt, Safe, pt)

       end    

   | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt

   | specify (Add_Find'  ct) p c pt = specify_additem "#Find"  ct p c pt

   | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt

   | specify (Specify_Theory' domID) (pos as (p,p_)) _ pt =

       let

         val p_ = case p_ of Met => Met | _ => Pbl

         val thy = assoc_thy domID

         val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of

           PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>

              (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)

         | _ => error "specify (Specify_Theory': uncovered case get_obj"

         val mppc = case p_ of Met => met | _ => pbl

         val cpI = if pI = e_pblID then pI' else pI

         val {prls = per, ppc, where_ = pwh, ...} = get_pbt cpI

         val cmI = if mI = e_metID then mI' else mI

         val {prls = mer, ppc = mpc, pre= mwh, ...} = get_met cmI

         val pre = case p_ of

           Met => (check_preconds thy mer mwh met)

         | _ => (check_preconds thy per pwh pbl)

         val pb = foldl and_ (true, map fst pre)

       in

         if domID = dI

         then

           let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)

 	        in

 	          ((p, p_), (pos, Uistate), 

 		        Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),

 		        nxt, Safe, pt)

           end

         else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)

 	        let 

 	          val ((p, p_), _, _, pt) = Ctree.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt

 	          val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)

 	        in

 	          ((p,p_), (pos,Uistate), 

 	          Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, length p, Ctree.Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),

 	          nxt, Safe, pt)

           end

       end

   | specify m' _ _ _ = error ("specify: not impl. for " ^ tac_2str m')

 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}

   -- for input from scratch*)

 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = 

     let

       val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of

         PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>

            (oris, dI', pI', dI, pI, pbl, ctxt)

       | _ => error "specify (Specify_Theory': uncovered case get_obj"

       val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

       val cpI = if pI = e_pblID then pI' else pI;

     in

       case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of

 	      Add itm (*..union old input *) =>

 	        let

 	          val pbl' = insert_ppc thy itm pbl

 	          val (tac, tac_) = case sel of

 		          "#Given" => (Add_Given    ct, Add_Given'   (ct, pbl'))

 		        | "#Find"  => (Add_Find     ct, Add_Find'    (ct, pbl'))

 		        | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))

 		        | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)

 		        val (p, Pbl, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of

 		          ((p, Pbl), c, _, pt') =>  (p, Pbl, c, pt')

 		        | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"

 	        in

 	          ([(tac, tac_, ((p, Pbl), (Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate' 

           end	       

 	    | Err msg => (*TODO.WN03 pass error-msgs to the frontend..

                      FIXME ..and dont abuse a tactic for that purpose*)

 	        ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),

 	          (e_pos', (e_istate, e_ctxt)))], [], ptp) 

     end

   | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) = 

     let

       val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of

         PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>

            (oris, dI', mI', dI, mI, met, ctxt)

       | _ => error "nxt_specif_additem Met: uncovered case get_obj"

       val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

       val cmI = if mI = e_metID then mI' else mI;

     in 

       case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of

         Add itm (*..union old input *) =>

 	        let

 	          val met' = insert_ppc thy itm met;

 	          val (tac,tac_) = case sel of

 		          "#Given" => (Add_Given    ct, Add_Given'   (ct, met'))

 		        | "#Find"  => (Add_Find     ct, Add_Find'    (ct, met'))

 		        | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))

 		        | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)

 	          val (p, Met, c, pt') = case Ctree.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of

 	            ((p, Met), c, _, pt') => (p, Met, c, pt')

 		        | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"

 	        in

 	          ([(tac, tac_, ((p, Met), (Uistate, ctxt)))], c, (pt', (p, Met)))

 	        end

       | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)

     end

   | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)

 fun ori2Coritm (pbt : pat list) ((i, v, f, d, ts) : ori) =

   ((i, v, true, f, Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts))) : itm)

     handle _ => ((i, v, true, f, Cor ((d, ts), (d, ts))) : itm)

       (*dsc in oris, but not in pbl pat list: keep this dsc*)

 (* filter out oris which have same description in itms *)

 fun filter_outs oris [] = oris

   | filter_outs oris (i::itms) = 

     let

       val ors = filter_out ((curry op = ((d_in o #5) (i:itm))) o (#4 : ori -> term)) oris

     in

       filter_outs ors itms

     end

 (* filter oris which are in pbt, too *)

 fun filter_pbt oris pbt =

   let

     val dscs = map (fst o snd) pbt

   in

     filter ((member op= dscs) o (#4 : ori -> term)) oris

   end

 (* combine itms from pbl + met and complete them wrt. pbt *)

 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)

 fun complete_metitms (oris : ori list) (pits : itm list) (mits: itm list) met = 

   let

     val vat = max_vt pits;

     val itms = pits @ (filter ((member_swap op = vat) o (#2 : itm -> int list)) mits)

     val ors = filter ((member_swap op= vat) o (#2 : ori -> int list)) oris

     val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)

   in

     itms @ (map (ori2Coritm met) os)

   end

 (* complete model and guard of a calc-head *)

 fun complete_mod_ (oris, mpc, ppc, probl) =

   let

     val pits = filter_out ((curry op= false) o (#3 : itm -> bool)) probl

     val vat = if probl = [] then 1 else max_vt probl

     val pors = filter ((member_swap op = vat) o (#2 : ori -> int list)) oris

     val pors = filter_outs pors pits (*which are in pbl already*)

     val pors = (filter_pbt pors ppc) (*which are in pbt, too*)

     val pits = pits @ (map (ori2Coritm ppc) pors)

     val mits = complete_metitms oris pits [] mpc

   in (pits, mits) end

 fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) =

   (if dI = e_domID then odI else dI,

    if pI = e_pblID then opI else pI,

    if mI = e_metID then omI else mI) : spec

 (* find a next applicable tac (for calcstate) and update ptree

  (for ev. finding several more tacs due to hide) *)

 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)

 (* WN.24.10.03        ~~~~~~~~~~~~~~   -> tac     -> tac_      -> -"- as arg *)

 (* WN.24.10.03        fun nxt_solv   = ...................................?? *)

 fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) =

     let

       val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of

         PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)

       | _ => error "nxt_specif Model_Problem; uncovered case get_obj"

       val (dI, pI, mI) = some_spec ospec spec

       val thy = assoc_thy dI

       val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)

       val {cas, ppc, ...} = get_pbt pI

       val pbl = Ctree.init_pbl ppc (* fill in descriptions *)

       (*----------------if you think, this should be done by the Dialog 

        in the java front-end, search there for WN060225-modelProblem----*)

       val (pbl, met) = case cas of

         NONE => (pbl, [])

   		| _ => complete_mod_ (oris, mpc, ppc, probl)

       (*----------------------------------------------------------------*)

       val tac_ = Model_Problem' (pI, pbl, met)

       val (pos,c,_,pt) = Ctree.generate1 thy tac_ (Uistate, ctxt) pos pt

     in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end

   | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp

   | nxt_specif (Add_Find  ct) ptp = nxt_specif_additem "#Find"  ct ptp

   | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp

     (*. called only if no_met is specified .*)     

   | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =

     let 

       val (oris, dI, ctxt) = case get_obj I pt p of

         (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)

       | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"

       val opt = refine_ori oris pI

     in 

       case opt of

 	      SOME pI' => 

 	        let 

             val {met, ...} = get_pbt pI'

 	          (*val pt = update_pbl pt p pbl ..done by Model_Problem*)

 	          val mI = if length met = 0 then e_metID else hd met

             val thy = assoc_thy dI

 	          val (pos, c, _, pt) = 

 		          Ctree.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt

 	        in

 	          ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),

 	              (pos, (Uistate, e_ctxt)))], c, (pt,pos)) 

           end

 	    | NONE => ([], [], ptp)

     end

   | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =

     let

       val (dI, dI', probl, ctxt) = case get_obj I pt p of

         PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>

           (dI, dI', probl, ctxt)

       | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"

 	    val thy = if dI' = e_domID then dI else dI'

     in 

       case refine_pbl (assoc_thy thy) pI probl of

 	      NONE => ([], [], ptp)

 	    | SOME rfd => 

 	      let 

           val (pos,c,_,pt) = Ctree.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt

 	      in

 	        ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))

         end

     end

   | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =

     let

       val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of

         PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...} =>

           (oris, dI, dI', pI', probl, ctxt)

       | _ => error ""

 	    val thy = assoc_thy (if dI' = e_domID then dI else dI');

       val {ppc,where_,prls,...} = get_pbt pI

 	    val pbl = 

 	      if pI' = e_pblID andalso pI = e_pblID

 	      then (false, (Ctree.init_pbl ppc, []))

 	      else match_itms_oris thy probl (ppc,where_,prls) oris

 	      (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)

 	    val (c, pt) = case Ctree.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of

 	      ((_, Pbl), c, _, pt) => (c, pt)

 	    | _ => error ""

     in

       ([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Uistate, e_ctxt)))], c, (pt,pos))

     end

   (* transfers oris (not required in pbl) to met-model for script-env

      FIXME.WN.8.03: application of several mIDs to SAME model?       *)

   | nxt_specif (Specify_Method mID) (pt, pos as (p,_)) = 

     let

       val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of

         PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}

           => (oris, pbl, dI, met, ctxt)

       | _ => error "nxt_specif Specify_Method: uncovered case get_obj"

       val {ppc,pre,prls,...} = get_met mID

       val thy = assoc_thy dI

       val oris = add_field' thy ppc oris

       val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)

       val (_, (itms, _)) = match_itms_oris thy met (ppc,pre,prls ) oris

       val (pos, c, _, pt) = 

 	      Ctree.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt

     in

       ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos)) 

     end    

   | nxt_specif (Specify_Theory dI) (pt, pos as (_, Pbl)) =

     let

       val ctxt = get_ctxt pt pos

 	    val (pos, c, _, pt) = 

 	      Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI)  (Uistate, ctxt) pos pt

     in (*FIXXXME: check if pbl can still be parsed*)

 	    ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,

 	      (pt, pos))

     end

   | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =

     let

       val ctxt = get_ctxt pt pos

 	    val (pos, c, _, pt) = Ctree.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt

     in  (*FIXXXME: check if met can still be parsed*)

 	    ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))

     end

   | nxt_specif m' _ = error ("nxt_specif: not impl. for "^tac2str m')

 (* get the values from oris; handle the term list w.r.t. penv *)

 fun vals_of_oris oris =

   ((map (mkval' o (#5 : ori -> term list))) o 

     (filter ((member_swap op= 1) o (#2 : ori -> int list)))) oris

 (* create a calc-tree with oris via an cas.refined pbl *)

 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =

     if pI <> [] 

     then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)

 	    let 

         val {cas, met, ppc, thy, ...} = get_pbt pI

 	      val dI = if dI = "" then theory2theory' thy else dI

 	      val mI = if mI = [] then hd met else mI

 	      val hdl = case cas of NONE => pblterm dI pI | SOME t => t

 	      val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))

 				  ([], (dI,pI,mI), hdl)

 	      val pt = update_spec pt [] (dI, pI, mI)

 	      val pits = Ctree.init_pbl' ppc

 	      val pt = update_pbl pt [] pits

 	    in ((pt, ([] , Pbl)), []) : calcstate end

     else 

       if mI <> [] 

       then (* from met-browser *)

 	      let 

           val {ppc, ...} = get_met mI

 	        val dI = if dI = "" then "Isac" else dI

 	        val (pt, _) =

 	          cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))

 	        val pt = update_spec pt [] (dI, pI, mI)

 	        val mits = Ctree.init_pbl' ppc

 	        val pt = update_met pt [] mits

 	      in ((pt, ([], Met)), []) end

       else (* new example, pepare for interactive modeling *)

 	      let

 	        val (pt, _) =

 	          cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)

 	      in ((pt, ([], Pbl)), []) end

   | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = 

     let           (* both """"""""""""""""""""""""" either empty or complete *)

 	    val thy = assoc_thy dI

 	    val (pI, (pors, pctxt), mI) = 

 	      if mI = ["no_met"] 

 	      then 

           let 

             val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;

 		        val pI' = refine_ori' pors pI;

 		      in (pI', (pors(*refinement over models with diff.precond only*), pctxt),

 		        (hd o #met o get_pbt) pI')

 		      end

 	      else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)

 	    val {cas, ppc, thy = thy', ...} = get_pbt pI (*take dI from _refined_ pbl*)

 	    val dI = theory2theory' (maxthy thy thy')

 	    val hdl = case cas of

 		    NONE => pblterm dI pI

 		  | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t

       val (pt, _) =

         cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)

       val pt = update_ctxt pt [] pctxt

     in

       ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate

     end

 fun get_spec_form m ((p, p_) : pos') pt = 

   let val (_, _, f, _, _, _) = specify m (p, p_) [] pt

   in f end

 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy

 	 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)

 fun tag_form thy (formal, given) =

  (let

     val gf = (head_of given) $ formal;

     val _ = Thm.global_cterm_of thy gf

   in gf end)

   handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^

     " .. " ^ term_to_string''' thy formal ^ " ..types do not match")

 fun chktyp thy (n, fs, gs) = 

   ((writeln o (term_to_string'''  thy) o (nth n)) fs;

    (writeln o (term_to_string''' thy) o (nth n)) gs;

    tag_form thy (nth n fs, nth n gs))

 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)

 (* check pbltypes, announces one failure a time *)

 fun chk_vars ctppc = 

   let

     val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)

     val chked = subtract op = gi wh

   in

     if chked <> [] then ("wh\\gi", chked)

     else

       let val chked = subtract op = (union op = gi fi) re

       in

         if chked  <> []

 	      then ("re\\(gi union fi)", chked)

 	      else ("ok", []) 

       end

   end

 (* check a new pbltype: variables (Free) unbound by given, find*) 

 fun unbound_ppc ctppc =

   let

     val {Given = gi, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)

   in

     distinct (subtract op = (union op = gi fi) re)

   end

 (* f, a binary operator, is nested right associative *)

 fun foldr1 f xs =

   let

     fun fld _ (x :: []) = x

       | fld f (x :: x' :: []) = f (x', x)

       | fld f (x :: x' :: xs) = f (fld f (x' :: xs), x)

       | fld _ _ = error "foldr1 uncovered definition"

   in ((fld f) o rev) xs end

 (* f, a binary operator, is nested leftassociative *)

 fun foldl1 _ (x :: []) = x

   | foldl1 f (x :: x' :: []) = f (x, x')

   | foldl1 f (x :: x' :: xs) = f (x, foldl1 f (x' :: xs))

   | foldl1 _ _ = error "foldl1 uncovered definition"

 (* called only once, if a Subproblem has been located in the script*)

 fun nxt_model_pbl (Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =

     (case metID of

        ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)

      | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))

        (*all stored in tac_ itms^^^^^^^^^^*)

   | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_)

 (* fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml *)

 fun eq4 v (_, vts, _, _, _) = member op = vts v

 fun eq5 (_, _, _, _, itm_) (_, _, _, d, _) = d_in itm_ = d

 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris

   + met from fmz; assumes pos on PblObj, meth = []                    *)

 fun complete_mod (pt, pos as (p, p_) : pos') =

   let

     val _ = if p_ <> Pbl 

 	    then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)

 	    else ()

 	  val (oris, ospec, probl, spec) = case get_obj I pt p of

 	    PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)

 	  | _ => error "complete_mod: unvered case get_obj"

   	val (_, pI, mI) = some_spec ospec spec

   	val mpc = (#ppc o get_met) mI

   	val ppc = (#ppc o get_pbt) pI

   	val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)

     val pt = update_pblppc pt p pits

 	  val pt = update_metppc pt p mits

   in (pt, (p, Met) : pos') end

 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);

    oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)

 fun all_modspec (pt, (p, _) : pos') =

   let

     val (pors, dI, pI, mI) = case get_obj I pt p of

       PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)

     | _ => error "all_modspec: uncovered case get_obj"

 	  val {ppc, ...} = get_met mI

     val (_, vals) = oris2fmz_vals pors

 	  val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 

       |> declare_constraints' vals

     val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)

 	  val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)

 	  val pt = update_spec pt p (dI, pI, mI)

     val pt = update_ctxt pt p ctxt

   in

     (pt, (p, Met) : pos')

   end

 (* WN0312: use in nxt_spec, too ? what about variants ??? *)

 fun is_complete_mod_ ([] : itm list) = false

   | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))

 fun is_complete_mod (pt, pos as (p, Pbl) : pos') =

     if (is_pblobj o (get_obj I pt)) p 

     then (is_complete_mod_ o (get_obj g_pbl pt)) p

     else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)

   | is_complete_mod (pt, pos as (p, Met)) = 

     if (is_pblobj o (get_obj I pt)) p 

     then (is_complete_mod_ o (get_obj g_met pt)) p

     else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)

   | is_complete_mod (_, pos) =

     error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")

 (* have (thy, pbl, met) _all_ been specified explicitly ? *)

 fun is_complete_spec (pt, pos as (p, _) : pos') = 

   if (not o is_pblobj o (get_obj I pt)) p 

   then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)

   else

     let val (dI,pI,mI) = get_obj g_spec pt p

     in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end

 (* complete empty items in specification from origin (pbl, met ev.refined);

    assumes 'is_complete_mod' *)

 fun complete_spec (pt, pos as (p, _) : pos') = 

   let

     val (ospec, spec) = case get_obj I pt p of

       PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)

     | _ => error "complete_spec: uncovered case get_obj"

     val pt = update_spec pt p (some_spec ospec spec)

   in

     (pt, pos)

   end

 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp

 fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =

     let

       val (_, _, metID) = get_somespec' spec spec'

 	    val pre = if metID = e_metID then []

 	      else

 	        let

 	          val {prls, pre= where_, ...} = get_met metID

 	          val pre = check_preconds' prls where_ meth 0

 		      in pre end

 	    val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))

     in

       ModSpec (allcorrect, Met, hdl, meth, pre, spec)

     end

   | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =

     let

       val (_, pI, _) = get_somespec' spec spec'

       val pre = if pI = e_pblID then []

 	      else

 	        let

 	          val {prls, where_, ...} = get_pbt pI

 	          val pre = check_preconds' prls where_ probl 0

 	        in pre end

 	    val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))

     in

       ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)

     end

   | pt_model _ _ = error "pt_model: uncovered definition"

 fun pt_form (PrfObj {form, ...}) = Form form

   | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =

     let

       val (dI, pI, _) = get_somespec' spec spec'

       val {cas, ...} = get_pbt pI

     in case cas of

       NONE => Form (pblterm dI pI)

     | SOME t => Form (subst_atomic (mk_env probl) t)

     end

 (* pt_extract returns

       # the formula at pos

       # the tactic applied to this formula

       # the list of assumptions generated at this formula

 	(by application of another tac to the preceding formula !)

    pos is assumed to come from the frontend, ie. generated by moveDown.

    Notes: cannot be in ctree.sml, because ModSpec has to be calculated. 

    TODO 110417 get assumptions from ctxt !?

 *)

 fun pt_extract (pt, ([], Res)) =

     (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)

     let

       val (f, asm) = get_obj g_result pt []

     in (Form f, NONE, asm) end

   | pt_extract (pt,(p,Res)) =

     let

       val (f, asm) = get_obj g_result pt p

       val tac =

         if last_onlev pt p

         then

           if is_pblobj' pt (lev_up p)

           then

             let

               val pI = case get_obj I pt (lev_up p) of

                 PblObj{spec = (_, pI, _), ...} => pI

               | _ => error "pt_extract last_onlev: uncovered case get_obj"

             in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end

 		      else SOME End_Trans (* WN0502 TODO for other branches *)

 		    else

 		      let val p' = lev_on p

 		      in

 		        if is_pblobj' pt p'

 		        then

 		          let

 		            val (dI ,pI) = case get_obj I pt p' of

 		              PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)

 		            | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"

 		          in SOME (Subproblem (dI, pI)) end

 		        else

 		          if f = get_obj g_form pt p'

 		          then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)

 		          else SOME (Take (term2str (get_obj g_form pt p')))

 		      end

     in (Form f, tac, asm) end

   | pt_extract (pt, (p,p_(*Frm,Pbl*))) =

       let

         val ppobj = get_obj I pt p

         val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p

         val tac = g_tac ppobj

       in (f, SOME tac, []) end

 (** get the formula from a ctree-node:

   take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)

   take res from all other PrfObj's

   Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)

 fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =

     [("headline", (p, Frm), h), ("stepform", (p, Res), r)]

   | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) = 

     [("stepform", (p, Frm), form), ("stepform", (p, Res), r)]

   | formres _ _ = error "formres: uncovered definition" 

 fun form p (Nd (PrfObj {result = (r, _), ...}, _)) = 

     [("stepform", (p, Res), r)]

   | form _ _ = error "form: uncovered definition" 

 (* assumes to take whole level, in particular hd -- for use in interSteps *)

 fun get_formress fs _ [] = flat fs

   | get_formress fs p (nd::nds) =

     (* start with   'form+res'       and continue with trying 'res' only*)

     get_forms (fs @ [formres p nd]) (lev_on p) nds

 and get_forms fs _ [] = flat fs

   | get_forms fs p (nd::nds) =

     if is_pblnd nd

     (* start again with      'form+res' ///ugly repeat with Check_elementwise

     then get_formress (fs @ [formres p nd]) (lev_on p) nds                   *)

     then get_forms    (fs @ [formres p nd]) (lev_on p) nds

     (* continue with trying 'res' only*)

     else get_forms    (fs @ [form    p nd]) (lev_on p) nds;

 (** get an 'interval' 'from' 'to' of formulae from a ptree **)

 (* WN0401 this functionality belongs to ctree.sml *)

 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2

   | eq_pos' (p1, Res) (p2, Res) = p1 = p2

   | eq_pos' (p1, Pbl) (p2, p2_) =

     p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)

   | eq_pos' (p1, Met) (p2, p2_) =

     p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)

   | eq_pos' _ _ = false;

 (* get an 'interval' from the ctree; 'interval' is w.r.t. the 

    total ordering Position#compareTo(Position p) in the java-code

 val get_interval = fn

     : pos' ->     : from is "move_up 1st-element" to return

       pos' -> 	  : to the last element to be returned; from < to

       int -> 	  : level: 0 gets the flattest sub-tree possible

 			   >999 gets the deepest sub-tree possible

       ptree -> 	  : 

       (pos' * 	  : of the formula

        Term.term) : the formula

 	  list                                                           *)

 fun get_interval from to level pt =

   let

     fun get_inter c (from : pos') (to : pos') lev pt =

 	    if eq_pos' from to orelse from = ([], Res)

 	    then

 	      let val (f, _, _) = pt_extract (pt, from)

 	      in case f of

 	        ModSpec (_,_,headline, _, _, _) => c @ [(from, headline)] 

 	      | Form t => c @ [(from, t)]

 	      end

 	    else 

 	      if lev < lev_of from

 	      then (get_inter c (move_dn [] pt from) to lev pt)

 		      handle (PTREE _(*from move_dn too far*)) => c

 		    else

 		      let

 		        val (f, _, _) = pt_extract (pt, from)

 		        val term = case f of

 		          ModSpec (_,_,headline,_,_,_) => headline

 				    | Form t => t

 		      in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)

 		        handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]

 		      end

   in get_inter [] from to level pt end

 (* for tests *)

 fun posform2str (pos : pos', form) =

   "(" ^ pos'2str pos ^ ", " ^

   (case form of Form f => term2str f | ModSpec c => term2str (#3 c(*the headline*))) ^

   ")"

 fun posforms2str pfs =

   (strs2str' o (map (curry op ^ "\n")) o (map posform2str)) pfs

 fun posterm2str (pos:pos', t) = "(" ^ pos'2str pos ^ ", " ^ term2str t ^ ")"

 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs

 (* WN050225 omits the last step, if pt is incomplete *)

 fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))

 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)

 fun get_ocalhd (pt, (p, Pbl) : pos') = 

     let

 	    val (ospec, hdf', spec, probl) = case get_obj I pt p of

 	      PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)

 	    | _ => error "get_ocalhd Pbl: uncovered case get_obj"

       val {prls, where_, ...} = get_pbt (#2 (some_spec ospec spec))

       val pre = check_preconds (assoc_thy"Isac") prls where_ probl

     in

       (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd

     end

   | get_ocalhd (pt, (p, Met)) = 

     let

 		  val (ospec, hdf', spec, meth) = case get_obj I pt p of

 		    PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)

 		  | _ => error "get_ocalhd Met: uncovered case get_obj"

       val {prls, pre, ...} = get_met (#3 (some_spec ospec spec))

       val pre = check_preconds (assoc_thy"Isac") prls pre meth

     in

       (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)

     end

   | get_ocalhd _ = error "get_ocalhd: uncovered definition"

 (* at the activeFormula set the Model, the Guard and the Specification 

    to empty and return a CalcHead;

    the 'origin' remains (for reconstructing all that) *)

 fun reset_calchead (pt, (p,_) : pos') = 

   let

     val () = case get_obj I pt p of

       PblObj _ => ()

     | _ => error "reset_calchead: uncovered case get_obj"

     val pt = update_pbl pt p []

     val pt = update_met pt p []

     val pt = update_spec pt p e_spec

   in (pt, (p, Pbl) : pos') end

 end