1.1 --- a/test/Tools/isac/Interpret/calchead.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/Interpret/calchead.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -406,10 +406,10 @@
     1.4  ============ inhibit exn AK110726 ==============================================*)
     1.5  "--------------------------------step through code mtc---";
     1.6  val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
     1.7 -cterm_of;
     1.8 +Thm.global_cterm_of;
     1.9  val ttt = (dsc $ var);
    1.10  (*============ inhibit exn AK110726 ==============================================
    1.11 -cterm_of thy (dsc $ var);
    1.12 +Thm.global_cterm_of thy (dsc $ var);
    1.13  ============ inhibit exn AK110726 ==============================================*)
    1.14  
    1.15  "-------------------------------------step through end---";
    1.16 @@ -497,10 +497,10 @@
    1.17  -------------------------------------------------------------------*)
    1.18  "--------------------------------step through code mtc---";
    1.19  val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
    1.20 -cterm_of;
    1.21 +Thm.global_cterm_of;
    1.22  val ttt = (dsc $ var);
    1.23  (*============ inhibit exn AK110726 ==============================================
    1.24 -cterm_of thy (dsc $ var);
    1.25 +Thm.global_cterm_of thy (dsc $ var);
    1.26  -------------------------------------------------------------------*)
    1.27  "-------------------------------------step through end---";
    1.28  
    1.29 @@ -554,7 +554,7 @@
    1.30  "--------------------------------step through code mtc---";
    1.31  val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
    1.32  val ttt = (dsc $ var);
    1.33 -cterm_of thy (dsc $ var);
    1.34 +Thm.global_cterm_of thy (dsc $ var);
    1.35  val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
    1.36  
    1.37  "-d2-----------------------------------------------------";
    1.38 @@ -567,7 +567,7 @@
    1.39  "--------------------------------step through code mtc---";
    1.40  val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
    1.41  val ttt = (dsc $ var);
    1.42 -cterm_of thy (dsc $ var);
    1.43 +Thm.global_cterm_of thy (dsc $ var);
    1.44  val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
    1.45  "-d3-----------------------------------------------------";
    1.46  pbt = [];  (*true, base case*)