1.1 --- a/src/Tools/isac/Interpret/generate.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    | init_istate (Rewrite_Set_Inst (subs, rls)) =
     1.5  (* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p);
     1.6     *)
     1.7 -    let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
     1.8 +    let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
     1.9      in case assoc_rls rls of
    1.10             Rls {scr=EmptyScr,...} => 
    1.11  	   error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
    1.12 @@ -67,7 +67,7 @@
    1.13  (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
    1.14     *)
    1.15    | init_istate (Rewrite_Set_Inst (subs, rls)) t =
    1.16 -    let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs
    1.17 +    let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
    1.18      (*...we suppose the substitution of only _one_ bound variable*)
    1.19      in case assoc_rls rls of
    1.20             Rls {scr=EmptyScr,...} => 
    1.21 @@ -330,7 +330,7 @@
    1.22         | NONE => 
    1.23  	 (pos,[],EmptyMout,update_env pt p (SOME is)))
    1.24  (* val (thy, (Take' t), l, (p,p_), pt) = 
    1.25 -       ((assoc_thy "Isac.thy"), tac_, is, pos, pt);
    1.26 +       ((assoc_thy "Isac"), tac_, is, pos, pt);
    1.27     *)
    1.28    | generate1 thy (Take' t) l (p,p_) pt = (* val (Take' t) = m; *)
    1.29    let (*val _=tracing("### generate1: Take' pos="^pos'2str (p,p_));*)
    1.30 @@ -343,7 +343,7 @@
    1.31  (* val (l, (p,p_)) = (RrlsState is, p);
    1.32  
    1.33     val (thy, Begin_Trans' t, l, (p,Frm), pt) =
    1.34 -       (assoc_thy "Isac.thy", tac_, is, p, pt);
    1.35 +       (assoc_thy "Isac", tac_, is, p, pt);
    1.36     *)
    1.37    | generate1 thy (Begin_Trans' t) l (p,Frm) pt =
    1.38    let (* print_depth 99;
    1.39 @@ -361,7 +361,7 @@
    1.40  				 term2str t)), pt) end
    1.41  
    1.42    (* val (thy, Begin_Trans' t, l, (p,Res), pt) =
    1.43 -	 (assoc_thy "Isac.thy", tac_, is, p, pt);
    1.44 +	 (assoc_thy "Isac", tac_, is, p, pt);
    1.45        *)
    1.46    | generate1 thy (Begin_Trans' t) l (p       ,Res) pt =
    1.47      (*append after existing PrfObj    _________*)
    1.48 @@ -395,7 +395,7 @@
    1.49  
    1.50    | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) l (p,p_) pt =
    1.51  (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) = 
    1.52 -       (assoc_thy "Isac.thy", tac_, is, pos, pt);
    1.53 +       (assoc_thy "Isac", tac_, is, pos, pt);
    1.54     *)
    1.55    let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
    1.56        val (pt,c) = cappend_atomic pt p l f 
    1.57 @@ -505,7 +505,7 @@
    1.58  	(* for recursion ...
    1.59  	 (tacis', (_, tac_, (p, is))) = split_last tacis';
    1.60  	 *)
    1.61 -	val (p',c',_,pt') = generate1 (assoc_thy "Isac.thy") tac_ is p pt
    1.62 +	val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
    1.63      in generate tacis' (pt', c@c', p') end;
    1.64  
    1.65