# HG changeset patch
# User wenzelm
# Date 962031175 -7200
# Node ID 4e06543e8b828112b35f83b94ac5ad3e438847e2
# Parent  9a64807da0235f1bf54d4688eddc85ace479bf58
bind_thm;

diff -r 9a64807da023 -r 4e06543e8b82 src/HOL/Lambda/Type.ML
--- a/src/HOL/Lambda/Type.ML	Mon Jun 26 16:18:51 2000 +0200
+++ b/src/HOL/Lambda/Type.ML	Mon Jun 26 16:52:55 2000 +0200
@@ -267,7 +267,7 @@
 by (Fast_tac 1);
 qed_spec_mp "subst_Var_IT";
 
-val Var_IT = rewrite_rule [mk_meta_eq foldl_Nil] (lists.Nil RS IT.VarI);
+bind_thm ("Var_IT", rewrite_rule [mk_meta_eq foldl_Nil] (lists.Nil RS IT.VarI));
 
 Goal "t : IT ==> t $ Var i : IT";
 by (etac IT.induct 1);