| changeset 8100 | 6186ee807f2e |
| parent 7040 | 613724c2ee6b |
| child 8438 | b8389b4fca9c |
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Jan 05 11:50:55 2000 +0100 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Wed Jan 05 11:56:04 2000 +0100 @@ -470,7 +470,7 @@ (* external interfaces *) fun read_term sg str = - read_cterm sg (str, HOLogic.termTVar); + read_cterm sg (str, HOLogic.termT); fun cert_term sg tm = cterm_of sg tm handle TERM (msg, _) => error msg;