1.1 --- a/src/Tools/isac/Interpret/appl.sml	Mon Dec 07 10:01:49 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Mon Dec 07 10:17:08 2015 +0100
     1.3 @@ -60,11 +60,11 @@
     1.4    end;
     1.5  
     1.6  val op_and = Const ("op &", [bool, bool] ---> bool);
     1.7 -(*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
     1.8 +(*> (Thm.global_cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
     1.9  val it = "a & b" : cterm
    1.10  *)
    1.11  fun mk_and a b = op_and $ a $ b;
    1.12 -(*> (cterm_of thy) 
    1.13 +(*> (Thm.global_cterm_of thy) 
    1.14       (mk_and (Free("a",bool)) (Free("b",bool)));
    1.15  val it = "a & b" : cterm*)
    1.16  
    1.17 @@ -76,7 +76,7 @@
    1.18      in mk t ts end;
    1.19  (*> val pred = map (term_of o the o (parse thy)) 
    1.20               ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
    1.21 -> (cterm_of thy) (mk_and pred);
    1.22 +> (Thm.global_cterm_of thy) (mk_and pred);
    1.23  val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
    1.24  
    1.25  
    1.26 @@ -177,7 +177,7 @@
    1.27  > val pred   = (term_of o the o (parse thy)) 
    1.28    "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
    1.29  > val ttt = check_elementwise thy consts (bdv, pred);
    1.30 -> (cterm_of thy) ttt;
    1.31 +> (Thm.global_cterm_of thy) ttt;
    1.32  val it = "[x = #-3, x = #3]" : cterm
    1.33  
    1.34  > val consts = (term_of o the o (parse thy)) "[x = #4]";
    1.35 @@ -185,7 +185,7 @@
    1.36  > val pred   = (term_of o the o (parse thy)) 
    1.37   "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
    1.38  > val ttt = check_elementwise thy consts (bdv,pred);
    1.39 -> (cterm_of thy) ttt;
    1.40 +> (Thm.global_cterm_of thy) ttt;
    1.41  val it = "[x = #4]" : cterm
    1.42  
    1.43  > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
    1.44 @@ -193,7 +193,7 @@
    1.45  > val pred   = (term_of o the o (parse thy))
    1.46   " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
    1.47  > val ttt = check_elementwise thy consts (bdv,pred);
    1.48 -> (cterm_of thy) ttt;
    1.49 +> (Thm.global_cterm_of thy) ttt;
    1.50  val it = "[]" : cterm*)
    1.51  
    1.52