1.1 --- a/src/Tools/isac/Interpret/inform.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -219,8 +219,8 @@
     1.4  	   in SOME (pt, (true, Met, hdt, mits, pre, spec):ocalhd) end
     1.5      end;
     1.6  
     1.7 -(*lazy evaluation for Isac.thy*)
     1.8 -fun Isac _  = assoc_thy "Isac.thy";
     1.9 +(*lazy evaluation for (theory "Isac")*)
    1.10 +fun Isac _  = assoc_thy "Isac";
    1.11  
    1.12  (*re-parse itms with a new thy and prepare for checking with ori list*)
    1.13  fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
    1.14 @@ -453,7 +453,7 @@
    1.15  		    let val pbt = (#ppc o get_pbt) pI
    1.16  			val dI' = #1 (some_spec ospec spec)
    1.17  			val oris = if pI = #2 ospec then oris 
    1.18 -				   else prep_ori fmz_(assoc_thy"Isac.thy") pbt;
    1.19 +				   else prep_ori fmz_(assoc_thy"Isac") pbt;
    1.20  		    in (Pbl, appl_adds dI' oris probl pbt 
    1.21  				       (map itms2fstr probl), meth) end else
    1.22  	       if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
    1.23 @@ -468,12 +468,12 @@
    1.24  	   val pt = update_spec pt p spec;
    1.25         in if pos_ = Pbl
    1.26  	  then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
    1.27 -		   val pre =check_preconds(assoc_thy"Isac.thy")prls where_ pits
    1.28 +		   val pre =check_preconds(assoc_thy"Isac")prls where_ pits
    1.29  	       in (update_pbl pt p pits,
    1.30  		   (ocalhd_complete pits pre spec, 
    1.31  		    Pbl, hdf', pits, pre, spec):ocalhd) end
    1.32  	  else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
    1.33 -		   val pre = check_preconds (assoc_thy"Isac.thy") prls pre mits
    1.34 +		   val pre = check_preconds (assoc_thy"Isac") prls pre mits
    1.35  	       in (update_met pt p mits,
    1.36  		   (ocalhd_complete mits pre spec, 
    1.37  		    Met, hdf', mits, pre, spec):ocalhd) end
    1.38 @@ -596,12 +596,12 @@
    1.39  
    1.40  fun mk_tacis ro erls (t, r as Thm _, (t', a)) = 
    1.41      (Rewrite (rule2thm' r), 
    1.42 -     Rewrite' ("Isac.thy", fst ro, erls, false, 
    1.43 +     Rewrite' ("Isac", fst ro, erls, false, 
    1.44  	       rule2thm' r, t, (t', a)),
    1.45       (e_pos'(*to be updated before generate tacis!!!*), Uistate))
    1.46    | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) = 
    1.47      (Rewrite_Set (rule2rls' r), 
    1.48 -     Rewrite_Set' ("Isac.thy", false, rls, t, (t', a)),
    1.49 +     Rewrite_Set' ("Isac", false, rls, t, (t', a)),
    1.50       (e_pos'(*to be updated before generate tacis!!!*), Uistate));
    1.51  
    1.52  (*fo = ifo excluded already in inform*)
    1.53 @@ -705,8 +705,8 @@
    1.54         (([],[],(pt,p)), (encode ifo));
    1.55     *)
    1.56  fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
    1.57 -    case parse (assoc_thy "Isac.thy") istr of
    1.58 -(* val SOME ifo = parse (assoc_thy "Isac.thy") istr;
    1.59 +    case parse (assoc_thy "Isac") istr of
    1.60 +(* val SOME ifo = parse (assoc_thy "Isac") istr;
    1.61     *)
    1.62  	SOME ifo =>
    1.63  	let val ifo = term_of ifo