1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed Nov 30 13:05:08 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Mon Dec 12 18:08:13 2016 +0100
     1.3 @@ -254,16 +254,16 @@
     1.4  	      if mI = ["no_met"] 
     1.5  	      then
     1.6            let
     1.7 -            val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
     1.8 +            val pors = (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
     1.9  		          handle ERROR "actual args do not match formal args" 
    1.10 -			        => (match_ags_msg pI stac ags(*raise exn*); [])
    1.11 +			        => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
    1.12  		        val pI' = refine_ori' pors pI;
    1.13  		      in (pI', pors (* refinement over models with diff.prec only *), 
    1.14  		          (hd o #met o get_pbt) pI') end
    1.15 -	      else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
    1.16 +	      else (pI, (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
    1.17  		      handle ERROR "actual args do not match formal args"
    1.18 -		      => (match_ags_msg pI stac ags(*raise exn*); []), mI);
    1.19 -      val (fmz_, vals) = oris2fmz_vals pors;
    1.20 +		      => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
    1.21 +      val (fmz_, vals) = Chead.oris2fmz_vals pors;
    1.22  	    val {cas,ppc,thy,...} = get_pbt pI
    1.23  	    val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
    1.24  	    val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
    1.25 @@ -271,7 +271,7 @@
    1.26  	    val hdl =
    1.27          case cas of
    1.28  		      NONE => pblterm dI pI
    1.29 -		    | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    1.30 +		    | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
    1.31        val f = subpbl (strip_thy dI) pI
    1.32      in (Subproblem (dI, pI),	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
    1.33      end
    1.34 @@ -416,16 +416,16 @@
    1.35  	      if mI = ["no_met"] 
    1.36  	      then
    1.37            let
    1.38 -            val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
    1.39 +            val pors = (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
    1.40  		          handle ERROR "actual args do not match formal args"
    1.41 -			          => (match_ags_msg pI stac ags(*raise exn*);[]);
    1.42 +			          => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);
    1.43  		        val pI' = refine_ori' pors pI;
    1.44  		      in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o get_pbt) pI')
    1.45            end
    1.46 -	      else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
    1.47 +	      else (pI, (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
    1.48  		      handle ERROR "actual args do not match formal args"
    1.49 -		      => (match_ags_msg pI stac ags(*raise exn*); []), mI);
    1.50 -      val (fmz_, vals) = oris2fmz_vals pors;
    1.51 +		      => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
    1.52 +      val (fmz_, vals) = Chead.oris2fmz_vals pors;
    1.53  	    val {cas, ppc, thy, ...} = get_pbt pI
    1.54  	    val dI = theory2theory' thy (*take dI from _refined_ pbl*)
    1.55  	    val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
    1.56 @@ -433,7 +433,7 @@
    1.57  	    val hdl = 
    1.58          case cas of
    1.59  		      NONE => pblterm dI pI
    1.60 -		    | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    1.61 +		    | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
    1.62        val f = subpbl (strip_thy dI) pI
    1.63      in 
    1.64        if domID = dI andalso pblID = pI
    1.65 @@ -676,13 +676,13 @@
    1.66                  AssOnly => (NasNap (v, E))
    1.67                | _ =>
    1.68                    (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
    1.69 -		                 Appl m' =>
    1.70 +		                 Chead.Appl m' =>
    1.71  		                   let
    1.72                           val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
    1.73  		                     val (p'',c',f',pt') =
    1.74  		                       generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
    1.75  		                   in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
    1.76 -		               | Notappl _ => (NasNap (v, E))
    1.77 +		               | Chead.Notappl _ => (NasNap (v, E))
    1.78  		              )
    1.79  		         )
    1.80           end)
    1.81 @@ -929,7 +929,7 @@
    1.82  	      Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
    1.83  	    | _ =>
    1.84          (case applicable_in p pt m of
    1.85 -		       Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
    1.86 +		       Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
    1.87  		     | _ => Napp E)
    1.88  	    end
    1.89  (*GOON*)