changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;

--- a/src/Pure/Isar/outer_lex.ML	Thu May 27 20:45:20 1999 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Thu May 27 20:47:30 1999 +0200
@@ -144,13 +144,13 @@
 
 val scan_verb =
   scan_blank ||
-  keep_line ($$ "|" --| Scan.ahead (Scan.one (not_equal "}"))) ||
-  keep_line (Scan.one (not_equal "|" andf Symbol.not_eof));
+  keep_line ($$ "*" --| Scan.ahead (Scan.one (not_equal "}"))) ||
+  keep_line (Scan.one (not_equal "*" andf Symbol.not_eof));
 
 val scan_verbatim =
-  keep_line ($$ "{" -- $$ "|") |--
+  keep_line ($$ "{" -- $$ "*") |--
     !! (lex_err (K "missing end of verbatim text"))
-      (change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "|" -- $$ "}")));
+      (change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "*" -- $$ "}")));
 
 
 (* scan space *)