# HG changeset patch
# User wenzelm
# Date 968172202 -7200
# Node ID bb848beb53f6c463e440550a4d5a09101364fde5
# Parent  1206c7615a47b173139c0e8bed424db13dad31ae
tuned;

diff -r 1206c7615a47 -r bb848beb53f6 doc-src/IsarRef/conversion.tex
--- a/doc-src/IsarRef/conversion.tex	Tue Sep 05 18:43:05 2000 +0200
+++ b/doc-src/IsarRef/conversion.tex	Tue Sep 05 18:43:22 2000 +0200
@@ -21,8 +21,8 @@
 %  \texttt{} & & \\
   \texttt{stac}~a~1 & & subst~a \\
   \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\
-  \texttt{split_all_tac} & & simp~(no_asm_simp)~only: split_paired_all & \Text{(HOL)} \\
-                         & \approx & simp~only: split_tupled_all & \Text{(HOL)} \\
+  \texttt{split_all_tac} & & simp~(no_asm_simp)~only:~split_tupled_all & \Text{(HOL)} \\
+                         & \approx & simp~only:~split_tupled_all & \Text{(HOL)} \\
                          & \ll & clarify & \Text{(HOL)} \\
 \end{matharray}
 
diff -r 1206c7615a47 -r bb848beb53f6 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Tue Sep 05 18:43:05 2000 +0200
+++ b/src/FOL/cladata.ML	Tue Sep 05 18:43:22 2000 +0200
@@ -9,12 +9,7 @@
 section "Classical Reasoner";
 
 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim_Data =
-struct
-  val classical = classical
-end;
-
-structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
+structure Make_Elim = Make_Elim_Fun(val classical = classical);
 
 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
   compatibliity with strange things done in many existing proofs *)
diff -r 1206c7615a47 -r bb848beb53f6 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Tue Sep 05 18:43:05 2000 +0200
+++ b/src/HOL/cladata.ML	Tue Sep 05 18:43:22 2000 +0200
@@ -32,12 +32,7 @@
 
 
 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim_Data =
-struct
-  val classical = classical
-end;
-
-structure Make_Elim = Make_Elim_Fun (Make_Elim_Data);
+structure Make_Elim = Make_Elim_Fun (val classical = classical);
 
 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
   compatibliity with strange things done in many existing proofs *)