1.1 --- a/src/Tools/isac/Interpret/appl.sml	Mon Dec 07 10:52:07 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Mon Dec 07 11:25:02 2015 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4      let fun mk t' (t::[]) = op_and $ t' $ t
     1.5  	  | mk t' (t::ts) = mk (op_and $ t' $ t) ts
     1.6      in mk t ts end;
     1.7 -(*> val pred = map (term_of o the o (parse thy)) 
     1.8 +(*> val pred = map (Thm.term_of o the o (parse thy)) 
     1.9               ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
    1.10  > (Thm.global_cterm_of thy) (mk_and pred);
    1.11  val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
    1.12 @@ -90,7 +90,7 @@
    1.13  	     then [pred] 
    1.14  	     else get_assumptions_ pt (p,Res))
    1.15  
    1.16 -(* val pred = (term_of o the o (parse thy)) pred;
    1.17 +(* val pred = (Thm.term_of o the o (parse thy)) pred;
    1.18     val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
    1.19     mk_set thy pt p consts pred;
    1.20     *)
    1.21 @@ -168,29 +168,29 @@
    1.22  val ct' = "HOL.True" : cterm'
    1.23  
    1.24  
    1.25 -> val const  = (term_of o the o (parse thy)) "(#3::real)";
    1.26 +> val const  = (Thm.term_of o the o (parse thy)) "(#3::real)";
    1.27  > val pred' = subst_atomic [(bdv,const)] pred;
    1.28  
    1.29  
    1.30 -> val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";
    1.31 -> val bdv    = (term_of o the o (parse thy)) "(x::real)";
    1.32 -> val pred   = (term_of o the o (parse thy)) 
    1.33 +> val consts = (Thm.term_of o the o (parse thy)) "[x = #-3, x = #3]";
    1.34 +> val bdv    = (Thm.term_of o the o (parse thy)) "(x::real)";
    1.35 +> val pred   = (Thm.term_of o the o (parse thy)) 
    1.36    "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
    1.37  > val ttt = check_elementwise thy consts (bdv, pred);
    1.38  > (Thm.global_cterm_of thy) ttt;
    1.39  val it = "[x = #-3, x = #3]" : cterm
    1.40  
    1.41 -> val consts = (term_of o the o (parse thy)) "[x = #4]";
    1.42 -> val bdv    = (term_of o the o (parse thy)) "(x::real)";
    1.43 -> val pred   = (term_of o the o (parse thy)) 
    1.44 +> val consts = (Thm.term_of o the o (parse thy)) "[x = #4]";
    1.45 +> val bdv    = (Thm.term_of o the o (parse thy)) "(x::real)";
    1.46 +> val pred   = (Thm.term_of o the o (parse thy)) 
    1.47   "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
    1.48  > val ttt = check_elementwise thy consts (bdv,pred);
    1.49  > (Thm.global_cterm_of thy) ttt;
    1.50  val it = "[x = #4]" : cterm
    1.51  
    1.52 -> val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
    1.53 -> val bdv    = (term_of o the o (parse thy)) "(x::real)";
    1.54 -> val pred   = (term_of o the o (parse thy))
    1.55 +> val consts = (Thm.term_of o the o (parse thy)) "[x = #-12 // #5]";
    1.56 +> val bdv    = (Thm.term_of o the o (parse thy)) "(x::real)";
    1.57 +> val pred   = (Thm.term_of o the o (parse thy))
    1.58   " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
    1.59  > val ttt = check_elementwise thy consts (bdv,pred);
    1.60  > (Thm.global_cterm_of thy) ttt;
    1.61 @@ -706,7 +706,7 @@
    1.62  				 ^f);*)
    1.63  	    val (id',f') = split_dummy (term2str f);
    1.64  	    (*val _= tracing("### applicable_in: f'= "^f');*)
    1.65 -	    (*val _= (term_of o the o (parse thy)) f';*)
    1.66 +	    (*val _= (Thm.term_of o the o (parse thy)) f';*)
    1.67  	    (*val _= tracing"### applicable_in: solve_equation_dummy";*)
    1.68  	  in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
    1.69  	     else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq