# HG changeset patch
# User oheimb
# Date 905352165 -7200
# Node ID f099dffd0f189e2a71de230adb51eae0378f74fe
# Parent  2e0c18eedfd099dc80ddce2ccd8af8ef7a64d8b6
removed superfluous AddIs thms (were already in)

diff -r 2e0c18eedfd0 -r f099dffd0f18 src/HOL/Sexp.ML
--- 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);