1.1 --- a/src/Tools/isac/Scripts/term_G.sml	Tue Aug 17 09:05:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Scripts/term_G.sml	Wed Aug 18 13:40:09 2010 +0200
     1.3 @@ -295,8 +295,8 @@
     1.4  fun mk_prop t = Trueprop $ t;
     1.5  val true_as_term = Const("True",bool);
     1.6  val false_as_term = Const("False",bool);
     1.7 -val true_as_cterm = cterm_of HOL true_as_term;
     1.8 -val false_as_cterm = cterm_of HOL false_as_term;
     1.9 +val true_as_cterm = cterm_of (theory "HOL") true_as_term;
    1.10 +val false_as_cterm = cterm_of (theory "HOL") false_as_term;
    1.11  
    1.12  infixr 5 -->;                    (*2002 /Pure/term.ML *)
    1.13  infixr --->;			 (*2002 /Pure/term.ML *)
    1.14 @@ -1255,11 +1255,10 @@
    1.15  ***   Free ( R, RealDef.real)                  *)
    1.16  
    1.17  (*version for testing local to theories*)
    1.18 -fun str2t thy str = (term_of o the o (parse thy )) str;
    1.19 -
    1.20 -fun str2term str = (term_of o the o (parse (assoc_thy "Isac.thy"))) str;
    1.21 -fun str2termN str = (term_of o the o (parseN (assoc_thy "Isac.thy"))) str;
    1.22 +fun str2term_ thy str = (term_of o the o (parse thy)) str;
    1.23 +fun str2term str = (term_of o the o (parse (theory "Isac"))) str;
    1.24  fun strs2terms ss = map str2term ss;
    1.25 +fun str2termN str = (term_of o the o (parseN (theory "Isac"))) str;
    1.26  
    1.27  (*+ makes a substitution from the output of Pattern.match +*)
    1.28  (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*)