tuned comments;

--- a/src/Pure/Isar/local_defs.ML	Thu Feb 02 12:52:20 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Feb 02 12:52:21 2006 +0100
@@ -90,12 +90,11 @@
   |> Thm.cterm_of (Thm.theory_of_cterm cprop);
 
 (*
-  [x]
-  [x == t]
-     :
-    B x
-  --------
-    B t
+  [x, x == t]
+       :
+      B x
+  -----------
+      B t
 *)
 fun def_export _ cprops thm =
   thm