| changeset 30304 | d8e4cd2ac2a1 |
| parent 28952 | 15a4b2cf8c34 |
| child 30450 | 7655e6533209 |
--- a/src/HOL/Tools/hologic.ML Thu Mar 05 08:23:10 2009 +0100 +++ b/src/HOL/Tools/hologic.ML Thu Mar 05 08:23:11 2009 +0100 @@ -225,7 +225,7 @@ fun dest_mem (Const ("op :", _) $ x $ A) = (x, A) | dest_mem t = raise TERM ("dest_mem", [t]); -fun mk_UNIV T = Const ("UNIV", mk_setT T); +fun mk_UNIV T = Const ("Set.UNIV", mk_setT T); (* binary operations and relations *)