# HG changeset patch
# User paulson
# Date 997275070 -7200
# Node ID c77e5401f2ffa18b93bdeccdbe6a20a2527c1f20
# Parent  0fba0357c04c8fe29b7d378b2f6bd5c58b082b57
get it working again using Hilbert_Choice

diff -r 0fba0357c04c -r c77e5401f2ff src/HOL/Induct/SList.thy
--- 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
 
diff -r 0fba0357c04c -r c77e5401f2ff src/HOL/Induct/Sexp.ML
--- a/src/HOL/Induct/Sexp.ML	Wed Aug 08 14:50:28 2001 +0200
+++ b/src/HOL/Induct/Sexp.ML	Wed Aug 08 14:51:10 2001 +0200
@@ -6,8 +6,6 @@
 S-expressions, general binary trees for defining recursive data structures
 *)
 
-open Sexp;
-
 (** sexp_case **)
 
 Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
diff -r 0fba0357c04c -r c77e5401f2ff src/HOL/Induct/Sexp.thy
--- a/src/HOL/Induct/Sexp.thy	Wed Aug 08 14:50:28 2001 +0200
+++ b/src/HOL/Induct/Sexp.thy	Wed Aug 08 14:51:10 2001 +0200
@@ -28,9 +28,9 @@
 defs
 
   sexp_case_def 
-   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
-                            | (? k.   M=Numb(k) & z=d(k))  
-                            | (? N1 N2. M = Scons N1 N2  & z=e N1 N2)"
+   "sexp_case c d e M == THE z. (EX x.   M=Leaf(x) & z=c(x))  
+                            | (EX k.   M=Numb(k) & z=d(k))  
+                            | (EX N1 N2. M = Scons N1 N2  & z=e N1 N2)"
 
   pred_sexp_def
      "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"