changeset 59621 | 291934bac95e |
parent 58950 | d07464875dd4 |
child 60363 | 5568b16aa477 |
--- 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;