diff -r c53c19fb22cb -r 7c6476c53a6c Sexp.ML
--- a/Sexp.ML	Thu Aug 18 12:07:51 1994 +0200
+++ b/Sexp.ML	Thu Aug 18 12:13:26 1994 +0200
@@ -1,7 +1,7 @@
 (*  Title: 	HOL/sexp
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 For sexp.thy.  S-expressions.
 *)
@@ -29,19 +29,19 @@
 
 (** Sexp_case **)
 
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(Leaf(a),c,d,e) = c(a)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, Leaf(a)) = c(a)";
 by (fast_tac (HOL_cs addIs  [select_equality] 
 	             addSDs [Leaf_inject]
 		     addSEs [Leaf_neq_Scons, Leaf_neq_Numb]) 1);
 val Sexp_case_Leaf = result();
 
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(Numb(k),c,d,e) = d(k)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, Numb(k)) = d(k)";
 by (fast_tac (HOL_cs addIs  [select_equality] 
 	             addSDs [Numb_inject]
 		     addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1);
 val Sexp_case_Numb = result();
 
-goalw Sexp.thy [Sexp_case_def] "Sexp_case(M$N, c, d, e) = e(M,N)";
+goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, M$N) = e(M,N)";
 by (fast_tac (HOL_cs addIs  [select_equality] 
 	             addSDs [Scons_inject]
 	             addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1);