| changeset 8100 | 6186ee807f2e |
| parent 7178 | 50b9849cf6ad |
| child 8154 | dab09e1ad594 |
--- a/src/HOL/Tools/record_package.ML Wed Jan 05 11:50:55 2000 +0100 +++ b/src/HOL/Tools/record_package.ML Wed Jan 05 11:56:04 2000 +0100 @@ -466,7 +466,7 @@ local -val sel_upd_pat = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s (u k r)", HOLogic.termTVar)]; +val sel_upd_pat = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s (u k r)", HOLogic.termT)]; fun proc sg _ t = (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>