diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Interpret/calchead.sml
--- a/test/Tools/isac/Interpret/calchead.sml	Mon Dec 07 11:32:12 2015 +0100
+++ b/test/Tools/isac/Interpret/calchead.sml	Mon Dec 07 14:10:59 2015 +0100
@@ -406,10 +406,10 @@
 ============ inhibit exn AK110726 ==============================================*)
 "--------------------------------step through code mtc---";
 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
-cterm_of;
+Thm.global_cterm_of;
 val ttt = (dsc $ var);
 (*============ inhibit exn AK110726 ==============================================
-cterm_of thy (dsc $ var);
+Thm.global_cterm_of thy (dsc $ var);
 ============ inhibit exn AK110726 ==============================================*)
 
 "-------------------------------------step through end---";
@@ -497,10 +497,10 @@
 -------------------------------------------------------------------*)
 "--------------------------------step through code mtc---";
 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
-cterm_of;
+Thm.global_cterm_of;
 val ttt = (dsc $ var);
 (*============ inhibit exn AK110726 ==============================================
-cterm_of thy (dsc $ var);
+Thm.global_cterm_of thy (dsc $ var);
 -------------------------------------------------------------------*)
 "-------------------------------------step through end---";
 
@@ -554,7 +554,7 @@
 "--------------------------------step through code mtc---";
 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
 val ttt = (dsc $ var);
-cterm_of thy (dsc $ var);
+Thm.global_cterm_of thy (dsc $ var);
 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
 
 "-d2-----------------------------------------------------";
@@ -567,7 +567,7 @@
 "--------------------------------step through code mtc---";
 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
 val ttt = (dsc $ var);
-cterm_of thy (dsc $ var);
+Thm.global_cterm_of thy (dsc $ var);
 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
 "-d3-----------------------------------------------------";
 pbt = [];  (*true, base case*)