changeset 41339 | 481c89fabcbc |
parent 40845 | 15b97bd4b5c0 |
child 41363 | 57ebe94c7fbf |
--- a/src/HOL/Tools/hologic.ML Tue Dec 21 06:53:20 2010 +0100 +++ b/src/HOL/Tools/hologic.ML Tue Dec 21 07:23:21 2010 +0100 @@ -8,6 +8,7 @@ sig val typeS: sort val typeT: typ + val mk_id: typ -> term val mk_comp: term * term -> term val boolN: string val boolT: typ @@ -145,6 +146,8 @@ (* functions *) +fun mk_id T = Const ("Fun.id", T --> T); + fun mk_comp (f, g) = let val fT = fastype_of f;