1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -1296,7 +1296,7 @@
     1.4        Model_Problem, Safe, pt) end
     1.5  
     1.6    | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
     1.7 -    let val (pos,_,_,pt) = generate1 (assoc_thy "Isac.thy") 
     1.8 +    let val (pos,_,_,pt) = generate1 (assoc_thy "Isac") 
     1.9  				     (Refine_Problem' rfd) Uistate pos pt
    1.10      in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd), 
    1.11  	Model_Problem, Safe, pt) end
    1.12 @@ -1629,7 +1629,7 @@
    1.13    | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
    1.14      let val (dI',_,_) = get_obj g_spec pt p
    1.15  	val (pos,c,_,pt) = 
    1.16 -	    generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI) 
    1.17 +	    generate1 (assoc_thy "Isac") (Specify_Theory' dI) 
    1.18  		      Uistate pos pt
    1.19      in  (*FIXXXME: check if pbl can still be parsed*)
    1.20  	([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
    1.21 @@ -1638,7 +1638,7 @@
    1.22    | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
    1.23      let val (dI',_,_) = get_obj g_spec pt p
    1.24  	val (pos,c,_,pt) = 
    1.25 -	    generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI) 
    1.26 +	    generate1 (assoc_thy "Isac") (Specify_Theory' dI) 
    1.27  		      Uistate pos pt
    1.28      in  (*FIXXXME: check if met can still be parsed*)
    1.29  	([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
    1.30 @@ -1678,7 +1678,7 @@
    1.31  	in ((pt,([],Pbl)), []): calcstate end
    1.32      else if mI <> [] then (*comes from met-browser*)
    1.33  	let val {ppc,...} = get_met mI
    1.34 -	    val dI = if dI = "" then "Isac.thy" else dI
    1.35 +	    val dI = if dI = "" then "Isac" else dI
    1.36  	    val thy = assoc_thy dI
    1.37  	    val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
    1.38  					 ([], (dI,pI,mI), e_term(*FIXME met*))
    1.39 @@ -2169,14 +2169,14 @@
    1.40      let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} = 
    1.41  	    get_obj I pt p
    1.42  	val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
    1.43 -	val pre = check_preconds (assoc_thy"Isac.thy") prls where_ probl
    1.44 +	val pre = check_preconds (assoc_thy"Isac") prls where_ probl
    1.45      in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
    1.46  | get_ocalhd (pt, pos' as (p,Met):pos') = 
    1.47      let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 
    1.48  		    spec, meth,...} = 
    1.49  	    get_obj I pt p
    1.50  	val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
    1.51 -	val pre = check_preconds (assoc_thy"Isac.thy") prls pre meth
    1.52 +	val pre = check_preconds (assoc_thy"Isac") prls pre meth
    1.53      in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
    1.54  
    1.55  (*.at the activeFormula set the Model, the Guard and the Specification