1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -347,7 +347,7 @@
     1.4  	val spec = (dI',pblID,mI')
     1.5  	val {ppc,where_,prls,...} = get_pbt pblID
     1.6  	val (model_ok, (pbl, pre)) = 
     1.7 -	    match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
     1.8 +	    match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
     1.9      in ModSpec (ocalhd_complete pbl pre spec,
    1.10  		Pbl, e_term, pbl, pre, spec) end;*)
    1.11  fun initcontext_pbl pt (pos as (p,_):pos') =
    1.12 @@ -359,7 +359,7 @@
    1.13  		    else pI'
    1.14  	val {ppc,where_,prls,...} = get_pbt pblID
    1.15  	val (model_ok, (pbl, pre)) = 
    1.16 -	    match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
    1.17 +	    match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
    1.18      in (model_ok, pblID, hdl, pbl, pre) end;
    1.19  
    1.20  fun initcontext_met pt (pos as (p,_):pos') =
    1.21 @@ -371,7 +371,7 @@
    1.22  		    else mI'
    1.23  	val {ppc,pre,prls,scr,...} = get_met metID
    1.24  	val (model_ok, (pbl, pre)) = 
    1.25 -	    match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os
    1.26 +	    match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
    1.27      in (model_ok, metID, scr, pbl, pre) end;
    1.28  
    1.29  (*.match the model of a problem at pos p 
    1.30 @@ -380,14 +380,14 @@
    1.31      let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
    1.32  	val {ppc,where_,prls,...} = get_pbt pI
    1.33  	val (model_ok, (pbl, pre)) = 
    1.34 -	    match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os
    1.35 +	    match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
    1.36      in (model_ok, pI, hdl, pbl, pre) end;
    1.37  
    1.38  fun context_met mI pt (p:pos) =
    1.39      let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p
    1.40  	val {ppc,pre,prls,scr,...} = get_met mI
    1.41  	val (model_ok, (pbl, pre)) = 
    1.42 -	    match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os
    1.43 +	    match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
    1.44      in (model_ok, mI, scr, pbl, pre) end
    1.45  
    1.46  
    1.47 @@ -395,10 +395,10 @@
    1.48     *)
    1.49  fun tryrefine pI pt (pos as (p,_):pos') =
    1.50      let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
    1.51 -    in case refine_pbl (assoc_thy "Isac.thy") pI probl of
    1.52 +    in case refine_pbl (assoc_thy "Isac") pI probl of
    1.53  	   NONE => (*copy from context_pbl*)
    1.54  	   let val {ppc,where_,prls,...} = get_pbt pI
    1.55 -	       val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy") 
    1.56 +	       val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") 
    1.57  						     probl (ppc,where_,prls) os
    1.58  	   in (false, pI, hdl, pbl, pre) end
    1.59  	 | SOME (pI, (pbl, pre)) => 
    1.60 @@ -437,7 +437,7 @@
    1.61  	 | ModSpec (_,p_, head, gfr, pre, _) => 
    1.62  	   Form' (PpcKF (0,EdUndef,0,Nundef,
    1.63  			 (case p_ of Pbl => Problem[] | Met => Method[],
    1.64 -			  itms2itemppc (assoc_thy"Isac.thy") gfr pre)))
    1.65 +			  itms2itemppc (assoc_thy"Isac") gfr pre)))
    1.66      end;
    1.67  
    1.68  (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;