src/HOL/Sum_Type.ML

--- a/src/HOL/Sum_Type.ML	Thu Feb 21 20:09:48 2002 +0100
+++ b/src/HOL/Sum_Type.ML	Thu Feb 21 20:10:05 2002 +0100
@@ -159,7 +159,7 @@
 by (Blast_tac 1);
 qed "Part_mono";
 
-val basic_monos = basic_monos @ [Part_mono];
+bind_thms ("basic_monos", basic_monos @ [Part_mono]);
 
 Goalw [Part_def] "a : Part A h ==> a : A";
 by (etac IntD1 1);