1.1 --- a/src/Tools/isac/ME/ctree.sml	Thu Aug 19 12:00:46 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/ctree.sml	Thu Aug 19 12:08:42 2010 +0200
     1.3 @@ -233,10 +233,10 @@
     1.4  	 (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o 
     1.5  	 (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*)
     1.6  fun subst2subs s = map (pair2str o 
     1.7 -			(apfst (Syntax.string_of_term (ctxt_Isac""))) o
     1.8 -			(apsnd (Syntax.string_of_term (ctxt_Isac"")))) s;
     1.9 -fun subst2subs' s = map ((apfst (Syntax.string_of_term (ctxt_Isac""))) o
    1.10 -			 (apsnd (Syntax.string_of_term (ctxt_Isac"")))) s;
    1.11 +			(apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o
    1.12 +			(apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s;
    1.13 +fun subst2subs' s = map ((apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o
    1.14 +			 (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s;
    1.15  fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
    1.16  (*> subs2subst thy ["(bdv,x)","(err,#0)"];
    1.17  val it =
    1.18 @@ -679,8 +679,8 @@
    1.19        "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
    1.20    | Rewrite_Set'(thy',pasm,rls',f,(f',asm))          
    1.21      => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","
    1.22 -    ^(Syntax.string_of_term (ctxt_Isac"") f)^",("^(Syntax.string_of_term (ctxt_Isac"") f')
    1.23 -    ^","^((strs2str o (map (Syntax.string_of_term (ctxt_Isac"")))) asm)^"))"
    1.24 +    ^(Syntax.string_of_term (thy2ctxt' "Isac") f)^",("^(Syntax.string_of_term (thy2ctxt' "Isac") f')
    1.25 +    ^","^((strs2str o (map (Syntax.string_of_term (thy2ctxt' "Isac")))) asm)^"))"
    1.26  
    1.27    | End_Detail' _             => "End_Detail' xxx"
    1.28    | Detail_Set' _             => "Detail_Set' xxx"
    1.29 @@ -724,8 +724,8 @@
    1.30    "\n("^(loc_2str l)^",("^(tac_2str m)^
    1.31    ",\n  ens= "^(subst2str eno)^
    1.32    ",\n  env= "^(subst2str env)^
    1.33 -  ",\n  iar= "^(Syntax.string_of_term (ctxt_Isac"") iar)^
    1.34 -  ",\n  res= "^(Syntax.string_of_term (ctxt_Isac"") res)^
    1.35 +  ",\n  iar= "^(Syntax.string_of_term (thy2ctxt' "Isac") iar)^
    1.36 +  ",\n  res= "^(Syntax.string_of_term (thy2ctxt' "Isac") res)^
    1.37    ",\n  "^(safe2str s)^"))";
    1.38  fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;
    1.39  
    1.40 @@ -852,16 +852,16 @@
    1.41  (* show hd origin or form only *)
    1.42  fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) = 
    1.43    ((pr_pos p) ^ " ----- pblobj -----\n")
    1.44 -(*   ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^
    1.45 -    (((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^
    1.46 +(*   ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
    1.47 +    (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
    1.48     "\n") *)
    1.49    | pr_short p (PrfObj {form = form,...}) =
    1.50    ((pr_pos p) ^ (term2str form) ^ "\n");
    1.51  (*
    1.52  fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) = 
    1.53    ((ints2str c) ^"   "^ 
    1.54 -   ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^
    1.55 -    (((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^
    1.56 +   ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
    1.57 +    (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
    1.58     "\n")
    1.59    | pr_cell p (PrfObj {cell = c, form = form,...}) =
    1.60    ((ints2str c) ^"   "^ (term2str form) ^ "\n");