--- a/src/HOL/Sexp.ML Wed Sep 09 16:21:08 1998 +0200
+++ b/src/HOL/Sexp.ML Wed Sep 09 16:42:45 1998 +0200
@@ -35,7 +35,7 @@
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
qed "sexp_In1I";
-AddIs (sexp.intrs@[SigmaI, uprodI]);
+AddIs sexp.intrs;
Goal "range(Leaf) <= sexp";
by (Blast_tac 1);