src/HOL/Sexp.ML

--- a/src/HOL/Sexp.ML	Thu Apr 13 15:01:45 2000 +0200
+++ b/src/HOL/Sexp.ML	Thu Apr 13 15:01:50 2000 +0200
@@ -49,7 +49,7 @@
 
 (** Introduction rules for 'pred_sexp' **)
 
-Goalw [pred_sexp_def] "pred_sexp <= sexp Times sexp";
+Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
 by (Blast_tac 1);
 qed "pred_sexp_subset_Sigma";