| changeset 59621 | 291934bac95e |
| parent 58354 | 04ac60da613e |
| child 59640 | a6d29266f01c |
--- a/src/HOL/Tools/TFL/thry.ML Fri Mar 06 14:01:08 2015 +0100 +++ b/src/HOL/Tools/TFL/thry.ML Fri Mar 06 15:58:56 2015 +0100 @@ -48,7 +48,7 @@ *---------------------------------------------------------------------------*) fun typecheck thry t = - Thm.cterm_of thry t + Thm.global_cterm_of thry t handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg | TERM (msg, _) => raise THRY_ERR "typecheck" msg;