src/HOL/ex/PiSets.thy

--- a/src/HOL/ex/PiSets.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/ex/PiSets.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -7,7 +7,7 @@
 Also the nice -> operator for function space
 *)
 
-PiSets = Univ + Finite +
+PiSets = Datatype_Universe + Finite +
 
 syntax
   "->" :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60)