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