src/ZF/IMP/Com.ML

--- a/src/ZF/IMP/Com.ML	Mon Dec 28 16:54:01 1998 +0100
+++ b/src/ZF/IMP/Com.ML	Mon Dec 28 16:54:53 1998 +0100
@@ -6,10 +6,6 @@
 
 open Com;
 
-val assign_type = prove_goalw Com.thy [assign_def]
-        "!!n. [| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat"
-    (fn _ => [ fast_tac (claset() addIs [apply_type,lam_type,if_type]) 1 ]);
-
 val type_cs = claset() addSDs [evala.dom_subset RS subsetD,
 			      evalb.dom_subset RS subsetD,
 			      evalc.dom_subset RS subsetD];