author | haftmann |
Tue, 21 Dec 2010 14:54:23 +0100 | |
changeset 41363 | 57ebe94c7fbf |
parent 41362 | 3cb30e525ee9 |
child 41366 | ea73e74ec827 |
--- a/src/HOL/Tools/hologic.ML Tue Dec 21 14:18:45 2010 +0100 +++ b/src/HOL/Tools/hologic.ML Tue Dec 21 14:54:23 2010 +0100 @@ -8,7 +8,7 @@ sig val typeS: sort val typeT: typ - val mk_id: typ -> term + val id_const: typ -> term val mk_comp: term * term -> term val boolN: string val boolT: typ @@ -146,7 +146,7 @@ (* functions *) -fun mk_id T = Const ("Fun.id", T --> T); +fun id_const T = Const ("Fun.id", T --> T); fun mk_comp (f, g) = let