# HG changeset patch
# User lcp
# Date 763904218 -3600
# Node ID 7738aed3f84dba0f393d0193d66f71ee9e544800
# Parent  523518f44286b7bfbca719aa9e9bccf35f0a1c74
Improved layout for inductive defs

diff -r 523518f44286 -r 7738aed3f84d src/ZF/List.ML
--- a/src/ZF/List.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/List.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -7,17 +7,15 @@
 *)
 
 structure List = Datatype_Fun
- (val thy = Univ.thy;
-  val rec_specs = 
-      [("list", "univ(A)",
-	  [(["Nil"],	"i"), 
-	   (["Cons"],	"[i,i]=>i")])];
-  val rec_styp = "i=>i";
-  val ext = None
-  val sintrs = 
-      ["Nil : list(A)",
-       "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
-  val monos = [];
+ (val thy        = Univ.thy
+  val rec_specs  = [("list", "univ(A)",
+                      [(["Nil"],    "i"), 
+                       (["Cons"],   "[i,i]=>i")])]
+  val rec_styp   = "i=>i"
+  val ext        = None
+  val sintrs     = ["Nil : list(A)",
+                    "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
+  val monos      = []
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/Acc.ML
--- a/src/ZF/ex/Acc.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/Acc.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -10,13 +10,12 @@
 *)
 
 structure Acc = Inductive_Fun
- (val thy = WF.thy addconsts [(["acc"],"i=>i")];
-  val rec_doms = [("acc", "field(r)")];
-  val sintrs = 
-      ["[| r-``{a} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
-  val monos = [Pow_mono];
-  val con_defs = [];
-  val type_intrs = [];
+ (val thy        = WF.thy addconsts [(["acc"],"i=>i")]
+  val rec_doms   = [("acc", "field(r)")]
+  val sintrs     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
+  val monos      = [Pow_mono]
+  val con_defs   = []
+  val type_intrs = []
   val type_elims = []);
 
 goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/Data.ML
--- a/src/ZF/ex/Data.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/Data.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -8,21 +8,20 @@
 *)
 
 structure Data = Datatype_Fun
- (val thy = Univ.thy;
-  val rec_specs = 
-      [("data", "univ(A Un B)",
-	  [(["Con0"],	"i"),
-	   (["Con1"],	"i=>i"),
-	   (["Con2"],	"[i,i]=>i"),
-	   (["Con3"],	"[i,i,i]=>i")])];
-  val rec_styp = "[i,i]=>i";
-  val ext = None
-  val sintrs = 
-	  ["Con0 : data(A,B)",
-	   "[| a: A |] ==> Con1(a) : data(A,B)",
-	   "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
-	   "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
-  val monos = [];
+ (val thy        = Univ.thy
+  val rec_specs  = [("data", "univ(A Un B)",
+                       [(["Con0"],   "i"),
+                        (["Con1"],   "i=>i"),
+                        (["Con2"],   "[i,i]=>i"),
+                        (["Con3"],   "[i,i,i]=>i")])]
+  val rec_styp   = "[i,i]=>i"
+  val ext        = None
+  val sintrs     = 
+          ["Con0 : data(A,B)",
+           "[| a: A |] ==> Con1(a) : data(A,B)",
+           "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
+           "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]
+  val monos      = []
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/LList.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,18 @@
 *)
 
 structure LList = CoDatatype_Fun
- (val thy = QUniv.thy;
-  val rec_specs = 
-      [("llist", "quniv(A)",
-	  [(["LNil"],	"i"), 
-	   (["LCons"],	"[i,i]=>i")])];
-  val rec_styp = "i=>i";
-  val ext = None
-  val sintrs = 
-      ["LNil : llist(A)",
-       "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
-  val monos = [];
+ (val thy        = QUniv.thy
+  val rec_specs  = [("llist", "quniv(A)",
+                      [(["LNil"],   "i"), 
+                       (["LCons"],  "[i,i]=>i")])]
+  val rec_styp   = "i=>i"
+  val ext        = None
+  val sintrs     = ["LNil : llist(A)",
+                    "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]
+  val monos      = []
   val type_intrs = codatatype_intrs
   val type_elims = codatatype_elims);
-  
+
 val [LNilI, LConsI] = LList.intrs;
 
 (*An elimination rule, for type-checking*)
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/LList_Eq.ML
--- a/src/ZF/ex/LList_Eq.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/LList_Eq.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -11,14 +11,14 @@
   a q/Q to the Sigma, Pair and converse rules.*)
 
 structure LList_Eq = CoInductive_Fun
- (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq", "llist(A) * llist(A)")];
-  val sintrs = 
-      ["<LNil, LNil> : lleq(A)",
-       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = LList.intrs@[SigmaI];
+ (val thy = LList.thy addconsts [(["lleq"],"i=>i")]
+  val rec_doms   = [("lleq", "llist(A) * llist(A)")]
+  val sintrs     = 
+        ["<LNil, LNil> : lleq(A)",
+         "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"]
+  val monos      = []
+  val con_defs   = []
+  val type_intrs = LList.intrs @ [SigmaI]
   val type_elims = [SigmaE2]);
 
 (** Alternatives for above:
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/ListN.ML
--- a/src/ZF/ex/ListN.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/ListN.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -10,14 +10,14 @@
 *)
 
 structure ListN = Inductive_Fun
- (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];
-  val rec_doms = [("listn", "nat*list(A)")];
-  val sintrs = 
-      ["<0,Nil> : listn(A)",
-       "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = nat_typechecks@List.intrs@[SigmaI]
+ (val thy        = ListFn.thy addconsts [(["listn"],"i=>i")]
+  val rec_doms   = [("listn", "nat*list(A)")]
+  val sintrs     = 
+          ["<0,Nil> : listn(A)",
+           "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
+  val monos      = []
+  val con_defs   = []
+  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
   val type_elims = [SigmaE2]);
 
 val listn_induct = standard 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/Primrec0.ML
--- a/src/ZF/ex/Primrec0.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/Primrec0.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -64,20 +64,20 @@
 (*** Inductive definition of the PR functions ***)
 
 structure Primrec = Inductive_Fun
- (val thy = Primrec0.thy;
-  val rec_doms = [("primrec", "list(nat)->nat")];
-  val ext = None
-  val sintrs = 
+ (val thy        = Primrec0.thy
+  val rec_doms   = [("primrec", "list(nat)->nat")]
+  val sintrs     = 
       ["SC : primrec",
        "k: nat ==> CONST(k) : primrec",
        "i: nat ==> PROJ(i) : primrec",
-       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
-       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
-  val monos = [list_mono];
-  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
+       "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
+       "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]
+  val monos      = [list_mono]
+  val con_defs   = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]
   val type_intrs = pr0_typechecks
   val type_elims = []);
 
+
 (* c: primrec ==> c: list(nat) -> nat *)
 val primrec_into_fun = Primrec.dom_subset RS subsetD;
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/TF.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,19 @@
 *)
 
 structure TF = Datatype_Fun
- (val thy = Univ.thy;
-  val rec_specs = 
-      [("tree", "univ(A)",
-	  [(["Tcons"],	"[i,i]=>i")]),
-       ("forest", "univ(A)",
-	  [(["Fnil"],	"i"),
-	   (["Fcons"],	"[i,i]=>i")])];
-  val rec_styp = "i=>i";
-  val ext = None
-  val sintrs = 
-	  ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
-	   "Fnil : forest(A)",
-	   "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
-  val monos = [];
+ (val thy        = Univ.thy
+  val rec_specs  = [("tree", "univ(A)",
+                       [(["Tcons"],  "[i,i]=>i")]),
+                    ("forest", "univ(A)",
+                       [(["Fnil"],   "i"),
+                        (["Fcons"],  "[i,i]=>i")])]
+  val rec_styp   = "i=>i"
+  val ext        = None
+  val sintrs     = 
+          ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
+           "Fnil : forest(A)",
+           "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
+  val monos      = []
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/acc.ML
--- a/src/ZF/ex/acc.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/acc.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -10,13 +10,12 @@
 *)
 
 structure Acc = Inductive_Fun
- (val thy = WF.thy addconsts [(["acc"],"i=>i")];
-  val rec_doms = [("acc", "field(r)")];
-  val sintrs = 
-      ["[| r-``{a} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
-  val monos = [Pow_mono];
-  val con_defs = [];
-  val type_intrs = [];
+ (val thy        = WF.thy addconsts [(["acc"],"i=>i")]
+  val rec_doms   = [("acc", "field(r)")]
+  val sintrs     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
+  val monos      = [Pow_mono]
+  val con_defs   = []
+  val type_intrs = []
   val type_elims = []);
 
 goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/data.ML
--- a/src/ZF/ex/data.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/data.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -8,21 +8,20 @@
 *)
 
 structure Data = Datatype_Fun
- (val thy = Univ.thy;
-  val rec_specs = 
-      [("data", "univ(A Un B)",
-	  [(["Con0"],	"i"),
-	   (["Con1"],	"i=>i"),
-	   (["Con2"],	"[i,i]=>i"),
-	   (["Con3"],	"[i,i,i]=>i")])];
-  val rec_styp = "[i,i]=>i";
-  val ext = None
-  val sintrs = 
-	  ["Con0 : data(A,B)",
-	   "[| a: A |] ==> Con1(a) : data(A,B)",
-	   "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
-	   "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
-  val monos = [];
+ (val thy        = Univ.thy
+  val rec_specs  = [("data", "univ(A Un B)",
+                       [(["Con0"],   "i"),
+                        (["Con1"],   "i=>i"),
+                        (["Con2"],   "[i,i]=>i"),
+                        (["Con3"],   "[i,i,i]=>i")])]
+  val rec_styp   = "[i,i]=>i"
+  val ext        = None
+  val sintrs     = 
+          ["Con0 : data(A,B)",
+           "[| a: A |] ==> Con1(a) : data(A,B)",
+           "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
+           "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]
+  val monos      = []
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/listn.ML
--- a/src/ZF/ex/listn.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/listn.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -10,14 +10,14 @@
 *)
 
 structure ListN = Inductive_Fun
- (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];
-  val rec_doms = [("listn", "nat*list(A)")];
-  val sintrs = 
-      ["<0,Nil> : listn(A)",
-       "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = nat_typechecks@List.intrs@[SigmaI]
+ (val thy        = ListFn.thy addconsts [(["listn"],"i=>i")]
+  val rec_doms   = [("listn", "nat*list(A)")]
+  val sintrs     = 
+          ["<0,Nil> : listn(A)",
+           "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
+  val monos      = []
+  val con_defs   = []
+  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
   val type_elims = [SigmaE2]);
 
 val listn_induct = standard 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/llist.ML
--- a/src/ZF/ex/llist.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/llist.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,18 @@
 *)
 
 structure LList = CoDatatype_Fun
- (val thy = QUniv.thy;
-  val rec_specs = 
-      [("llist", "quniv(A)",
-	  [(["LNil"],	"i"), 
-	   (["LCons"],	"[i,i]=>i")])];
-  val rec_styp = "i=>i";
-  val ext = None
-  val sintrs = 
-      ["LNil : llist(A)",
-       "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
-  val monos = [];
+ (val thy        = QUniv.thy
+  val rec_specs  = [("llist", "quniv(A)",
+                      [(["LNil"],   "i"), 
+                       (["LCons"],  "[i,i]=>i")])]
+  val rec_styp   = "i=>i"
+  val ext        = None
+  val sintrs     = ["LNil : llist(A)",
+                    "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]
+  val monos      = []
   val type_intrs = codatatype_intrs
   val type_elims = codatatype_elims);
-  
+
 val [LNilI, LConsI] = LList.intrs;
 
 (*An elimination rule, for type-checking*)
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/llist_eq.ML
--- a/src/ZF/ex/llist_eq.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/llist_eq.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -11,14 +11,14 @@
   a q/Q to the Sigma, Pair and converse rules.*)
 
 structure LList_Eq = CoInductive_Fun
- (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq", "llist(A) * llist(A)")];
-  val sintrs = 
-      ["<LNil, LNil> : lleq(A)",
-       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
-  val monos = [];
-  val con_defs = [];
-  val type_intrs = LList.intrs@[SigmaI];
+ (val thy = LList.thy addconsts [(["lleq"],"i=>i")]
+  val rec_doms   = [("lleq", "llist(A) * llist(A)")]
+  val sintrs     = 
+        ["<LNil, LNil> : lleq(A)",
+         "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"]
+  val monos      = []
+  val con_defs   = []
+  val type_intrs = LList.intrs @ [SigmaI]
   val type_elims = [SigmaE2]);
 
 (** Alternatives for above:
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/primrec0.ML
--- a/src/ZF/ex/primrec0.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/primrec0.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -64,20 +64,20 @@
 (*** Inductive definition of the PR functions ***)
 
 structure Primrec = Inductive_Fun
- (val thy = Primrec0.thy;
-  val rec_doms = [("primrec", "list(nat)->nat")];
-  val ext = None
-  val sintrs = 
+ (val thy        = Primrec0.thy
+  val rec_doms   = [("primrec", "list(nat)->nat")]
+  val sintrs     = 
       ["SC : primrec",
        "k: nat ==> CONST(k) : primrec",
        "i: nat ==> PROJ(i) : primrec",
-       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
-       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
-  val monos = [list_mono];
-  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
+       "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
+       "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]
+  val monos      = [list_mono]
+  val con_defs   = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]
   val type_intrs = pr0_typechecks
   val type_elims = []);
 
+
 (* c: primrec ==> c: list(nat) -> nat *)
 val primrec_into_fun = Primrec.dom_subset RS subsetD;
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/ex/tf.ML
--- a/src/ZF/ex/tf.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/ex/tf.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -7,20 +7,19 @@
 *)
 
 structure TF = Datatype_Fun
- (val thy = Univ.thy;
-  val rec_specs = 
-      [("tree", "univ(A)",
-	  [(["Tcons"],	"[i,i]=>i")]),
-       ("forest", "univ(A)",
-	  [(["Fnil"],	"i"),
-	   (["Fcons"],	"[i,i]=>i")])];
-  val rec_styp = "i=>i";
-  val ext = None
-  val sintrs = 
-	  ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
-	   "Fnil : forest(A)",
-	   "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
-  val monos = [];
+ (val thy        = Univ.thy
+  val rec_specs  = [("tree", "univ(A)",
+                       [(["Tcons"],  "[i,i]=>i")]),
+                    ("forest", "univ(A)",
+                       [(["Fnil"],   "i"),
+                        (["Fcons"],  "[i,i]=>i")])]
+  val rec_styp   = "i=>i"
+  val ext        = None
+  val sintrs     = 
+          ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
+           "Fnil : forest(A)",
+           "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
+  val monos      = []
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/fin.ML
--- a/src/ZF/fin.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/fin.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -18,13 +18,12 @@
 *)
 
 structure Fin = Inductive_Fun
- (val thy = Arith.thy addconsts [(["Fin"],"i=>i")];
-  val rec_doms = [("Fin","Pow(A)")];
-  val sintrs = 
-	  ["0 : Fin(A)",
-	   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"];
-  val monos = [];
-  val con_defs = [];
+ (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]
+  val rec_doms   = [("Fin","Pow(A)")]
+  val sintrs     = ["0 : Fin(A)",
+                    "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
+  val monos      = []
+  val con_defs   = []
   val type_intrs = [empty_subsetI, cons_subsetI, PowI]
   val type_elims = [make_elim PowD]);
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/list.ML
--- a/src/ZF/list.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/list.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -7,17 +7,15 @@
 *)
 
 structure List = Datatype_Fun
- (val thy = Univ.thy;
-  val rec_specs = 
-      [("list", "univ(A)",
-	  [(["Nil"],	"i"), 
-	   (["Cons"],	"[i,i]=>i")])];
-  val rec_styp = "i=>i";
-  val ext = None
-  val sintrs = 
-      ["Nil : list(A)",
-       "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
-  val monos = [];
+ (val thy        = Univ.thy
+  val rec_specs  = [("list", "univ(A)",
+                      [(["Nil"],    "i"), 
+                       (["Cons"],   "[i,i]=>i")])]
+  val rec_styp   = "i=>i"
+  val ext        = None
+  val sintrs     = ["Nil : list(A)",
+                    "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
+  val monos      = []
   val type_intrs = datatype_intrs
   val type_elims = datatype_elims);
 
diff -r 523518f44286 -r 7738aed3f84d src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/simpdata.ML	Thu Mar 17 12:36:58 1994 +0100
@@ -86,9 +86,6 @@
       | _ $ A => tryrules atomize_pairs A
   end;
 
-fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
-
-
 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
 		beta, eta, restrict, fst_conv, snd_conv, split];
 
@@ -99,6 +96,6 @@
    [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
 
 val ZF_ss = FOL_ss 
-      setmksimps ZF_mk_rew_rules
+      setmksimps (map mk_meta_eq o atomize o gen_all)
       addsimps (ZF_simps @ mem_simps @ bquant_simps)
       addcongs ZF_congs;