# HG changeset patch
# User wenzelm
# Date 1189018105 -7200
# Node ID e8197c9f1b5cdb2ea2bfda77dada5060e46f9f2f
# Parent  888d56a8d9d344d784c207eaa3fbeefbf5a438b9
tuned;

diff -r 888d56a8d9d3 -r e8197c9f1b5c src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Sep 05 15:46:32 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed Sep 05 20:48:25 2007 +0200
@@ -4,7 +4,7 @@
 Miscellaneous examples for Higher-Order Logic.
 *)
 
-no_document use_thys  [
+no_document use_thys [
   "Parity",
   "GCD"
 ];