# HG changeset patch
# User wenzelm
# Date 1138881141 -3600
# Node ID efd9d44a0bdb02ab896b472b259cdea73866acf6
# Parent  324bcc35570d144906fb1eebba102d5c6044aeff
tuned comments;

diff -r 324bcc35570d -r efd9d44a0bdb src/Pure/Isar/local_defs.ML
--- 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