1.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Apr 07 16:31:05 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Fri Apr 08 15:16:08 2011 +0200
     1.3 @@ -280,9 +280,9 @@
     1.4  fun appl_add' dI oris ppc pbt (sel, ct) = 
     1.5      let 
     1.6        val ctxt = assoc_thy dI |> thy2ctxt;
     1.7 -    in case parse (ProofContext.theory_of ctxt) ct of
     1.8 +    in case parseNEW ctxt ct of
     1.9  	   NONE => (0,[],false,sel, Syn ct):itm
    1.10 -	 | SOME ct => (case is_known ctxt sel oris (term_of ct) of
    1.11 +	 | SOME t => (case is_known ctxt sel oris t of
    1.12           ("", ori', all) =>
    1.13             (case is_notyet_input ctxt ppc all ori' pbt of
    1.14  	         ("",itm)  => itm