diff -r 2488337fd0dd -r cac1f942e1a1 src/sml/IsacKnowledge/Integrate.thy
--- a/src/sml/IsacKnowledge/Integrate.thy	Sat Aug 20 19:10:30 2005 +0200
+++ b/src/sml/IsacKnowledge/Integrate.thy	Sat Aug 20 21:20:16 2005 +0200
@@ -27,7 +27,7 @@
 
   (*Script-names*)
   IntegrationScript      :: "[real,real,  real] => real"
-                  ("((Script IntegrationScript (_ _=))// (_))" 9)
+                  ("((Script IntegrationScript (_ _ =))// (_))" 9)
   NamedIntegrationScript :: "[real,real,real,  bool] => bool"
                   ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)