1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Mon Dec 07 10:01:49 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Mon Dec 07 10:17:08 2015 +0100
     1.3 @@ -812,7 +812,7 @@
     1.4      (* val (thy, (str, (dsc, _)), (ty $ var)) =
     1.5  	   (thy,  p,               a);
     1.6         *)
     1.7 -    (cterm_of thy (dsc $ var);(*type check*)
     1.8 +    (Thm.global_cterm_of thy (dsc $ var);(*type check*)
     1.9       SOME ((([1], str, dsc, (*[var]*)
    1.10  	    split_dts' (dsc, var))): preori)(*:ori without leading #*))
    1.11      handle e as TYPE _ => 
    1.12 @@ -1532,12 +1532,12 @@
    1.13        in f end;
    1.14  
    1.15  
    1.16 -(*fun tag_form thy (formal, given) = cterm_of thy
    1.17 +(*fun tag_form thy (formal, given) = Thm.global_cterm_of thy
    1.18  	      (((head_of o term_of) given) $ (term_of formal)); WN100819*)
    1.19  fun tag_form thy (formal, given) =
    1.20   (let
    1.21      val gf = (head_of given) $ formal;
    1.22 -    val _ = cterm_of thy gf
    1.23 +    val _ = Thm.global_cterm_of thy gf
    1.24    in gf end)
    1.25    handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
    1.26      " .. " ^ term_to_string''' thy formal ^ " ..types do not match");
    1.27 @@ -1632,9 +1632,9 @@
    1.28    in ((fld f) o rev) xs end;
    1.29  (*
    1.30  > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
    1.31 -> val ces = map (cterm_of thy) (isalist2list (term_of ct));
    1.32 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
    1.33  > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
    1.34 -> cterm_of thy conj;
    1.35 +> Thm.global_cterm_of thy conj;
    1.36  val it = "(a = b & c = d) & e = f" : cterm
    1.37  *)
    1.38  
    1.39 @@ -1644,9 +1644,9 @@
    1.40    | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
    1.41  (*
    1.42  > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
    1.43 -> val ces = map (cterm_of thy) (isalist2list (term_of ct));
    1.44 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
    1.45  > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
    1.46 -> cterm_of thy conj;
    1.47 +> Thm.global_cterm_of thy conj;
    1.48  val it = "a = b & c = d & e = f & g = h" : cterm
    1.49  *)
    1.50