diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/Scripts/term_G.sml
--- a/src/Tools/isac/Scripts/term_G.sml	Tue Aug 17 09:05:51 2010 +0200
+++ b/src/Tools/isac/Scripts/term_G.sml	Wed Aug 18 13:40:09 2010 +0200
@@ -295,8 +295,8 @@
 fun mk_prop t = Trueprop $ t;
 val true_as_term = Const("True",bool);
 val false_as_term = Const("False",bool);
-val true_as_cterm = cterm_of HOL true_as_term;
-val false_as_cterm = cterm_of HOL false_as_term;
+val true_as_cterm = cterm_of (theory "HOL") true_as_term;
+val false_as_cterm = cterm_of (theory "HOL") false_as_term;
 
 infixr 5 -->;                    (*2002 /Pure/term.ML *)
 infixr --->;			 (*2002 /Pure/term.ML *)
@@ -1255,11 +1255,10 @@
 ***   Free ( R, RealDef.real)                  *)
 
 (*version for testing local to theories*)
-fun str2t thy str = (term_of o the o (parse thy )) str;
-
-fun str2term str = (term_of o the o (parse (assoc_thy "Isac.thy"))) str;
-fun str2termN str = (term_of o the o (parseN (assoc_thy "Isac.thy"))) str;
+fun str2term_ thy str = (term_of o the o (parse thy)) str;
+fun str2term str = (term_of o the o (parse (theory "Isac"))) str;
 fun strs2terms ss = map str2term ss;
+fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str;
 
 (*+ makes a substitution from the output of Pattern.match +*)
 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*)