diff -r bb75c1cdf913 -r c839b38a1f32 doc-src/IsarImplementation/Thy/unused.thy
--- a/doc-src/IsarImplementation/Thy/unused.thy	Mon Sep 04 15:27:30 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/unused.thy	Mon Sep 04 16:28:27 2006 +0200
@@ -1,6 +1,17 @@
 
 text {*
 
+  
+
+  A \emph{fixed variable} acts like a local constant in the current
+  context, representing some simple type @{text "\<alpha>"}, or some value
+  @{text "x: \<tau>"} (for a fixed type expression @{text "\<tau>"}).  A
+  \emph{schematic variable} acts like a placeholder for arbitrary
+  elements, similar to outermost quantification.  The division between
+  fixed and schematic variables tells which abstract entities are
+  inside and outside the current context.
+
+
   @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\