src/HOL/Tools/TFL/casesplit.ML

--- a/src/HOL/Tools/TFL/casesplit.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/TFL/casesplit.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -37,8 +37,8 @@
       val x = Free(vstr,ty)
       val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
 
-      val ctermify = Thm.cterm_of sgn;
-      val ctypify = Thm.ctyp_of sgn;
+      val ctermify = Thm.global_cterm_of sgn;
+      val ctypify = Thm.global_ctyp_of sgn;
       val case_thm = case_thm_of_ty sgn ty;
 
       val abs_ct = ctermify abst;