diff -r 872f866e630f -r d9527f97246e ex/Simult.ML
--- a/ex/Simult.ML	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Simult.ML	Thu Aug 25 10:47:33 1994 +0200
@@ -3,13 +3,11 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For Simult.thy.
-
 Primitives for simultaneous recursive type definitions
   includes worked example of trees & forests
 
 This is essentially the same data structure that on ex/term.ML, which is
-simpler because it uses List as a new type former.  The approach in this
+simpler because it uses list as a new type former.  The approach in this
 file may be superior for other simultaneous recursions.
 *)
 
@@ -29,15 +27,15 @@
 by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
 val TF_mono = result();
 
-goalw Simult.thy [TF_def] "TF(Sexp) <= Sexp";
+goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [Sexp_NumbI,Sexp_In0I,Sexp_In1I,Sexp_SconsI]
+by (fast_tac (univ_cs addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
                       addSEs [PartE]) 1);
-val TF_Sexp = result();
+val TF_sexp = result();
 
-(* A <= Sexp ==> TF(A) <= Sexp *)
-val TF_subset_Sexp = standard
-    (TF_mono RS (TF_Sexp RSN (2,subset_trans)));
+(* A <= sexp ==> TF(A) <= sexp *)
+val TF_subset_sexp = standard
+    (TF_mono RS (TF_sexp RSN (2,subset_trans)));
 
 
 (** Elimination -- structural induction on the set TF **)
@@ -51,8 +49,7 @@
 \    !!M N. [| M:  Part(TF(A),In0);  N: Part(TF(A),In1);  R(M);  R(N) \
 \            |] ==> R(FCONS(M,N))    \
 \    |] ==> R(i)";
-by (rtac (major RS (TF_def RS def_induct)) 1);
-by (rtac TF_fun_mono 1);
+by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
 by (fast_tac (set_cs addIs (prems@[PartI])
 		       addEs [usumE, uprodE, PartE]) 1);
 val TF_induct = result();
@@ -228,19 +225,19 @@
 val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE);
 
 
-(*** TF_rec -- by wf recursion on pred_Sexp ***)
+(*** TF_rec -- by wf recursion on pred_sexp ***)
 
 val TF_rec_unfold =
-    wf_pred_Sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+    wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
 
 (** conversion rules for TF_rec **)
 
 goalw Simult.thy [TCONS_def]
-    "!!M N. [| M: Sexp;  N: Sexp |] ==> 	\
+    "!!M N. [| M: sexp;  N: sexp |] ==> 	\
 \           TF_rec(TCONS(M,N),b,c,d) = b(M, N, TF_rec(N,b,c,d))";
 by (rtac (TF_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps [Case_In0, Split]) 1);
-by (asm_simp_tac (pred_Sexp_ss addsimps [In0_def]) 1);
+by (asm_simp_tac (pred_sexp_ss addsimps [In0_def]) 1);
 val TF_rec_TCONS = result();
 
 goalw Simult.thy [FNIL_def] "TF_rec(FNIL,b,c,d) = c";
@@ -249,29 +246,29 @@
 val TF_rec_FNIL = result();
 
 goalw Simult.thy [FCONS_def]
- "!!M N. [| M: Sexp;  N: Sexp |] ==> 	\
+ "!!M N. [| M: sexp;  N: sexp |] ==> 	\
 \        TF_rec(FCONS(M,N),b,c,d) = d(M, N, TF_rec(M,b,c,d), TF_rec(N,b,c,d))";
 by (rtac (TF_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
-by (asm_simp_tac (pred_Sexp_ss addsimps [CONS_def,In1_def]) 1);
+by (asm_simp_tac (pred_sexp_ss addsimps [CONS_def,In1_def]) 1);
 val TF_rec_FCONS = result();
 
 
 (*** tree_rec, forest_rec -- by TF_rec ***)
 
-val Rep_Tree_in_Sexp =
-    [range_Leaf_subset_Sexp RS TF_subset_Sexp RS (Part_subset RS subset_trans),
+val Rep_Tree_in_sexp =
+    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
      Rep_Tree] MRS subsetD;
-val Rep_Forest_in_Sexp =
-    [range_Leaf_subset_Sexp RS TF_subset_Sexp RS (Part_subset RS subset_trans),
+val Rep_Forest_in_sexp =
+    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
      Rep_Forest] MRS subsetD;
 
 val tf_rec_simps = [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
 		    TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
 		    Rep_Tree_inverse, Rep_Forest_inverse,
 		    Abs_Tree_inverse, Abs_Forest_inverse,
-		    inj_Leaf, Inv_f_f, Sexp_LeafI, range_eqI,
-		    Rep_Tree_in_Sexp, Rep_Forest_in_Sexp];
+		    inj_Leaf, Inv_f_f, sexp.LeafI, range_eqI,
+		    Rep_Tree_in_sexp, Rep_Forest_in_sexp];
 val tf_rec_ss = HOL_ss addsimps tf_rec_simps;
 
 goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]