# HG changeset patch
# User paulson
# Date 844941623 -7200
# Node ID e2ec077ac90d856ae3832896b9163987f9bcb99c
# Parent  e814e03bbbb206c323e48ec1b7c910e65dda67ff
Deleted obsolete clasets

diff -r e814e03bbbb2 -r e2ec077ac90d src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Oct 10 11:59:01 1996 +0200
+++ b/src/HOL/Prod.ML	Thu Oct 10 12:00:23 1996 +0200
@@ -299,12 +299,6 @@
         fst_imageE, snd_imageE, prod_fun_imageE,
         Pair_inject];
 
-val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] 
-                     addIs  [fst_imageI, snd_imageI, prod_fun_imageI]
-                     addSEs [SigmaE2, SigmaE, splitE, mem_splitE, 
-                             fst_imageE, snd_imageE, prod_fun_imageE,
-                             Pair_inject];
-
 structure Prod_Syntax =
 struct
 
diff -r e814e03bbbb2 -r e2ec077ac90d src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Thu Oct 10 11:59:01 1996 +0200
+++ b/src/HOL/Sexp.ML	Thu Oct 10 12:00:23 1996 +0200
@@ -38,8 +38,6 @@
 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
 qed "sexp_In1I";
 
-val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
-
 AddIs (sexp.intrs@[SigmaI, uprodI]);
 
 goal Sexp.thy "range(Leaf) <= sexp";