| changeset 8100 | 6186ee807f2e |
| parent 7481 | d44c77be268c |
| child 8141 | d6d896e81cd7 |
--- a/src/HOL/Tools/typedef_package.ML Wed Jan 05 11:50:55 2000 +0100 +++ b/src/HOL/Tools/typedef_package.ML Wed Jan 05 11:56:04 2000 +0100 @@ -89,7 +89,7 @@ (* prepare_typedef *) fun read_term sg used s = - #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termTVar)); + #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT)); fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;