1.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Dec 19 09:02:41 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Mon Dec 19 10:37:44 2016 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature LUCAS_INTERPRETER =
     1.5  sig
     1.6  
     1.7 -  type step = tac_ * Ctree.mout * ptree * pos' * pos' list
     1.8 +  type step = tac_ * Generate.mout * ptree * pos' * pos' list
     1.9    datatype locate = NotLocatable | Steps of istate * step list
    1.10    
    1.11    val next_tac : (*diss: next-tactic-function*)
    1.12 @@ -61,7 +61,7 @@
    1.13     Assoc (scrstate, steps) => ... ass* scrstate steps *)
    1.14  type step =
    1.15      tac_         (*transformed from associated tac                   *)
    1.16 -    * Ctree.mout (*result with indentation etc.                      *)
    1.17 +    * Generate.mout (*result with indentation etc.                      *)
    1.18      * ptree      (*containing node created by tac_ + resp. scrstate  *)
    1.19      * pos'       (*position in ptree; ptree * pos' is the proofstate *)
    1.20      * pos' list; (*of ptree-nodes probably cut (by fst tac_)         *)
    1.21 @@ -80,7 +80,7 @@
    1.22  	      val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
    1.23  	      val is = RrlsState (f', f'', rss, rts)
    1.24  	      val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
    1.25 -	      val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt
    1.26 +	      val (p', cid, mout, pt') = Generate.generate1 thy m (is, ctxt) p pt
    1.27        in (is, (m, mout, pt', p', cid) :: steps) end
    1.28    | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') =
    1.29        let
    1.30 @@ -89,7 +89,7 @@
    1.31  	      val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
    1.32  	      val is = RrlsState (f', f'', rss, rts)
    1.33  	      val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
    1.34 -	      val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt
    1.35 +	      val (p', cid, mout, pt') = Generate.generate1 thy m (is, ctxt) p pt
    1.36        in rts2steps ((m, mout, pt', p', cid)::steps) 
    1.37  		    ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts'
    1.38  		  end
    1.39 @@ -665,11 +665,11 @@
    1.40             case assod pt d m stac of
    1.41  	         Ass (m,v') =>
    1.42  	           let val (p'',c',f',pt') =
    1.43 -                 Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
    1.44 +                 Generate.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
    1.45  	           in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
    1.46             | AssWeak (m,v') => 
    1.47  	           let val (p'',c',f',pt') =
    1.48 -               Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
    1.49 +               Generate.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
    1.50  	           in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
    1.51             | NotAss =>
    1.52               (case ap of   (*switch for Or: 1st AssOnly, 2nd AssGen*)
    1.53 @@ -680,7 +680,7 @@
    1.54  		                   let
    1.55                           val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
    1.56  		                     val (p'',c',f',pt') =
    1.57 -		                       Ctree.generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p', p_) pt;
    1.58 +		                       Generate.generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p', p_) pt;
    1.59  		                   in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
    1.60  		               | Chead.Notappl _ => (NasNap (v, E))
    1.61  		              )
    1.62 @@ -822,8 +822,8 @@
    1.63      let val thy = assoc_thy thy';
    1.64      in case if l = [] orelse (
    1.65  		       (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res)
    1.66 -	       then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) body)
    1.67 -	       else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) ) of
    1.68 +	       then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) body)
    1.69 +	       else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) ) of
    1.70  	    Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) =>
    1.71  	      (if strong_ass
    1.72           then (Steps (ScrState is, ss))
    1.73 @@ -833,7 +833,7 @@
    1.74               let
    1.75                 val (po,p_) = p
    1.76                 val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_)
    1.77 -               val (p'',c'',f'',pt'') = Ctree.generate1 thy m (ScrState is, ctxt) (po',p_) pt
    1.78 +               val (p'',c'',f'',pt'') = Generate.generate1 thy m (ScrState is, ctxt) (po',p_) pt
    1.79  	           in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
    1.80  	         else Steps (ScrState is, ss))
    1.81