--- a/ex/Term.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/Term.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -29,7 +29,7 @@
 qed "term_sexp";
 
 (* A <= sexp ==> term(A) <= sexp *)
-val term_subset_sexp = standard ([term_mono, term_sexp] MRS subset_trans);
+bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans));
 
 
 (** Elimination -- structural induction on the set term(A) **)