1.1 --- a/test/Tools/isac/Interpret/inform.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/Interpret/inform.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -1018,7 +1018,7 @@
     1.4  "~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
     1.5    (cs', (encode ifo));
     1.6  val 	SOME f_in = parse (assoc_thy "Isac") istr
     1.7 -val f_in = term_of f_in
     1.8 +val f_in = Thm.term_of f_in
     1.9  val pos_pred = lev_back' pos
    1.10  			(* f_pred ---"step pos cs"---> f_succ in appendFormula
    1.11     TODO.WN120517: one starting point for redesign of pos' *)