src/HOL/Auth/Message_lemmas.ML

 
 Goal "H \\<subseteq> parts(H)";
 by (Blast_tac 1);
 qed "parts_increasing";
 
-val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
+bind_thm ("parts_insertI", impOfSubs (subset_insertI RS parts_mono));
 
 Goal "parts{} = {}";
 by Safe_tac;
 by (etac parts.induct 1);
 by (ALLGOALS Blast_tac);