1.1 --- a/src/Tools/isac/Interpret/solve.sml	Wed Nov 30 13:05:08 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Mon Dec 12 18:08:13 2016 +0100
     1.3 @@ -157,7 +157,7 @@
     1.4  		          generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
     1.5  			        (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
     1.6  	          in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt), 
     1.7 -		          ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate') 
     1.8 +		          ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)) : Chead.calcstate') 
     1.9  	          end	      
    1.10  	      | NONE => (*execute the first tac in the Script, compare solve m*)
    1.11  	          let
    1.12 @@ -276,7 +276,7 @@
    1.13        let
    1.14          val {srls,ppc,...} = get_met mI;
    1.15          val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
    1.16 -        val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
    1.17 +        val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
    1.18          val thy' = get_obj g_domID pt p;
    1.19          val thy = assoc_thy thy';
    1.20          val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = Lucin.init_scrstate thy itms mI;
    1.21 @@ -289,7 +289,7 @@
    1.22  	            val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
    1.23  	            val (pos,c,_,pt) = (*implicit Take*)
    1.24  	              generate1 thy tac_ (is, ctxt) pos pt
    1.25 -            in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
    1.26 +            in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)) : Chead.calcstate' end
    1.27          | NONE =>
    1.28              let
    1.29                val pt = update_env pt (fst pos) (SOME (is, ctxt))
    1.30 @@ -355,7 +355,7 @@
    1.31  (* find the next tac from the script, nxt_solv will update the ptree *)
    1.32  and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
    1.33        if e_metID = get_obj g_metID pt (par_pblobj pt p)
    1.34 -      then ([], [], (pt,(p,p_))):calcstate'
    1.35 +      then ([], [], (pt, (p, p_))) : Chead.calcstate'
    1.36        else 
    1.37          let 
    1.38            val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.39 @@ -395,7 +395,7 @@
    1.40      if member op = [Pbl,Met] p_
    1.41      then
    1.42        let
    1.43 -        val ptp = all_modspec ptp
    1.44 +        val ptp = Chead.all_modspec ptp
    1.45  	      val (_, c', ptp) = all_solve auto c ptp
    1.46  	    in complete_solve auto (c @ c') ptp end
    1.47      else
    1.48 @@ -405,7 +405,7 @@
    1.49            then ("ok", c @ c', ptp)
    1.50  	        else
    1.51              let
    1.52 -              val ptp = all_modspec ptp'
    1.53 +              val ptp = Chead.all_modspec ptp'
    1.54  	           val (_, c'', ptp) = all_solve auto (c @ c') ptp
    1.55  	         in complete_solve auto (c @ c'@ c'') ptp end
    1.56  	    | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
    1.57 @@ -469,12 +469,12 @@
    1.58     *)
    1.59  fun get_form ((mI,m):tac'_) ((p,p_):pos') pt = 
    1.60    case applicable_in (p,p_) pt m of
    1.61 -    Notappl e => Error' (Error_ e)
    1.62 -  | Appl m => 
    1.63 +    Chead.Notappl e => Error' (Error_ e)
    1.64 +  | Chead.Appl m => 
    1.65        (* val Appl m=applicable_in (p,p_) pt m;
    1.66           *)
    1.67        if member op = specsteps mI
    1.68 -	then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
    1.69 +	then let val (_,_,f,_,_,_) = Chead.specify m (p,p_) [] pt
    1.70  	     in f end
    1.71        else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
    1.72  	   in (*f*) EmptyMout end;