1.1 --- a/src/Tools/isac/Interpret/appl.sml	Thu Apr 07 16:31:05 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Fri Apr 08 15:16:08 2011 +0200
     1.3 @@ -595,8 +595,8 @@
     1.4         then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
     1.5       else
     1.6         let val thy' = get_obj g_domID pt (par_pblobj pt p);
     1.7 -       in (case parse (assoc_thy thy') ct' of
     1.8 -	       SOME ct => Appl (Take' (term_of ct))
     1.9 +       in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
    1.10 +	       SOME ct => Appl (Take' ct)
    1.11  	     | NONE => Notappl ("syntax error in "^ct'))
    1.12         end
    1.13  
    1.14 @@ -699,7 +699,7 @@
    1.15                Frm => (get_obj g_form pt p , [])
    1.16  	    | Res => get_obj g_result pt p;
    1.17      (*val _= tracing("### applicable_in Check_elementwise: f= "^f);*)
    1.18 -    val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred);
    1.19 +    val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
    1.20      (*val (v,p)=vp;val _=tracing("### applicable_in Check_elementwise: vp= "^
    1.21  			       pair2str(term2str v,term2str p))*)
    1.22    in case f of
    1.23 @@ -763,7 +763,7 @@
    1.24  	    (*val _= (term_of o the o (parse thy)) f';*)
    1.25  	    (*val _= tracing"### applicable_in: solve_equation_dummy";*)
    1.26  	  in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
    1.27 -	     else if is_expliceq ((term_of o the o (parse thy)) f')
    1.28 +	     else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq
    1.29  		      then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
    1.30  		  else error ("applicable_in: f= " ^ f') end
    1.31      | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end