--- a/src/HOL/Sexp.thy Tue Jun 04 12:49:04 1996 +0200 +++ b/src/HOL/Sexp.thy Thu Jun 06 13:13:18 1996 +0200 @@ -18,7 +18,7 @@ pred_sexp :: "('a item * 'a item)set" -inductive "sexp" +inductive sexp intrs LeafI "Leaf(a): sexp" NumbI "Numb(i): sexp"