1.1 --- a/src/Tools/isac/Interpret/inform.sml	Wed Apr 06 18:01:02 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu Apr 07 16:31:05 2011 +0200
     1.3 @@ -279,12 +279,12 @@
     1.4     *)
     1.5  fun appl_add' dI oris ppc pbt (sel, ct) = 
     1.6      let 
     1.7 -	val ctxt = assoc_thy dI |> thy2ctxt;
     1.8 -	in case parseNEW ctxt ct of
     1.9 +      val ctxt = assoc_thy dI |> thy2ctxt;
    1.10 +    in case parse (ProofContext.theory_of ctxt) ct of
    1.11  	   NONE => (0,[],false,sel, Syn ct):itm
    1.12 -	 | SOME t => (case is_known ctxt sel oris t of
    1.13 -	     ("", ori', all) =>
    1.14 -	       (case is_notyet_input ctxt ppc all ori' pbt of
    1.15 +	 | SOME ct => (case is_known ctxt sel oris (term_of ct) of
    1.16 +         ("", ori', all) =>
    1.17 +           (case is_notyet_input ctxt ppc all ori' pbt of
    1.18  	         ("",itm)  => itm
    1.19  	       | (msg,_) => error ("appl_add': " ^ msg))
    1.20       | (_, (i, v, _, d, ts), _) => if is_e_ts ts then