--- a/src/HOL/Induct/SList.thy Wed Aug 08 14:50:28 2001 +0200
+++ b/src/HOL/Induct/SList.thy Wed Aug 08 14:51:10 2001 +0200
@@ -10,7 +10,7 @@
so that list can serve as a "functor" for defining other recursive types
*)
-SList = Sexp +
+SList = Sexp + Hilbert_Choice (*gives us "inv"*) +
consts