--- 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);