# HG changeset patch
# User wenzelm
# Date 1153398937 -7200
# Node ID 42473922812349b28aca5e2294467478b9a4cc54
# Parent  6ff853f82d739181c62eb53cc73796e913cd91c3
removed Variable.monomorphic;

diff -r 6ff853f82d73 -r 424739228123 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Jul 20 14:34:57 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Jul 20 14:35:37 2006 +0200
@@ -49,7 +49,6 @@
   \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context -> thm list * Proof.context| \\
   \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   \indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\
-  \indexml{Variable.monomorphic}\verb|Variable.monomorphic: Proof.context -> term list -> term list| \\
   \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
   \end{mldecls}
 
@@ -84,9 +83,6 @@
   \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|, i.e.\ it provides a view on facts with all
   variables being fixed in the current context.
 
-  \item \verb|Variable.monomorphic|~\isa{ctxt\ ts} introduces fixed
-  type variables for the schematic ones in \isa{ts}.
-
   \item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type
   variables in \isa{ts} as far as possible, even those occurring
   in fixed term variables.  This operation essentially reverses the
diff -r 6ff853f82d73 -r 424739228123 doc-src/IsarImplementation/Thy/proof.thy
--- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Jul 20 14:34:57 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Jul 20 14:35:37 2006 +0200
@@ -18,7 +18,6 @@
   @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\
   @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
   @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
-  @{index_ML Variable.monomorphic: "Proof.context -> term list -> term list"} \\
   @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
   \end{mldecls}
 
@@ -56,9 +55,6 @@
   Variable.export}, i.e.\ it provides a view on facts with all
   variables being fixed in the current context.
 
-  \item @{ML Variable.monomorphic}~@{text "ctxt ts"} introduces fixed
-  type variables for the schematic ones in @{text "ts"}.
-
   \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
   variables in @{text "ts"} as far as possible, even those occurring
   in fixed term variables.  This operation essentially reverses the