1.1 --- a/src/Tools/isac/Interpret/inform.sml	Mon Dec 07 10:52:07 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon Dec 07 11:25:02 2015 +0100
     1.3 @@ -187,11 +187,11 @@
     1.4      in itm end
     1.5      handle _ => ((i,v,false,f, Syn (term2str t)):itm))
     1.6    | parsitm dI (itm as (i,v,b,f, Syn str)) =
     1.7 -    (let val t = (term_of o the o (parse dI)) str
     1.8 +    (let val t = (Thm.term_of o the o (parse dI)) str
     1.9      in (i,v,b,f, Par str) end
    1.10      handle _ => (i,v,b,f, Syn str))
    1.11    | parsitm dI (itm as (i,v,b,f, Typ str)) =
    1.12 -    (let val t = (term_of o the o (parse dI)) str
    1.13 +    (let val t = (Thm.term_of o the o (parse dI)) str
    1.14       in (i,v,b,f, Par str) end
    1.15       handle _ => (i,v,b,f, Syn str))
    1.16    | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
    1.17 @@ -263,7 +263,7 @@
    1.18  	 | SOME ct => 
    1.19  (* val SOME ct = parse thy str;
    1.20     *)
    1.21 -	   let val (d,ts) = (split_dts o term_of) ct
    1.22 +	   let val (d,ts) = (split_dts o Thm.term_of) ct
    1.23  	       val popt = find_first (eq7 (f,d)) pbt
    1.24  	   in case popt of
    1.25  		  NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
    1.26 @@ -663,7 +663,7 @@
    1.27    case parse (assoc_thy "Isac") istr of
    1.28  	  SOME f_in =>
    1.29  	    let
    1.30 -	      val f_in = term_of f_in
    1.31 +	      val f_in = Thm.term_of f_in
    1.32  	      val f_succ = get_curr_formula (pt, pos);
    1.33  			in
    1.34  			  if f_succ = f_in