# HG changeset patch
# User wenzelm
# Date 847978321 -3600
# Node ID 35ade49419047bf9a66ce373180badef48af6081
# Parent  f9686e7e6d4d65234ed931b503047059c1cb3bfa
removed silly message;

diff -r f9686e7e6d4d -r 35ade4941904 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Nov 14 14:31:29 1996 +0100
+++ b/src/Pure/Syntax/parser.ML	Thu Nov 14 14:32:01 1996 +0100
@@ -1,6 +1,6 @@
 (*  Title:      Pure/Syntax/parser.ML
     ID:         $Id$
-    Author:     Sonia Mahjoub, Markus Wenzel, and Carsten Clasohm, TU Muenchen
+    Author:     Carsten Clasohm, Sonia Mahjoub, and Markus Wenzel, TU Muenchen
 
 Isabelle's main parser (used for terms and types).
 *)
@@ -487,8 +487,6 @@
     val (nt_count', prod_count', tags', xprods') =
       prod_of xprods nt_count prod_count tags [];
 
-    val dummy = writeln "Building new grammar...";
-
     (*Copy array containing productions of old grammar;
       this has to be done to preserve the old grammar while being able
       to change the array's content*)
@@ -512,8 +510,6 @@
 (*Merge two grammars*)
 fun merge_grams gram_a gram_b =
   let
-    val dummy = writeln "Building new grammar...";
-
     (*find out which grammar is bigger*)
     val (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1,
                chains = chains1, lambdas = lambdas1, prods = prods1},