# HG changeset patch
# User wenzelm
# Date 1014318605 -3600
# Node ID b7b0daf0d8821f90c1f66df0b31de27c45a156f9
# Parent  32292d83367be3b8ed825388b7df69fbcebbd4f2
bind_thms basic_monos;

diff -r 32292d83367b -r b7b0daf0d882 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);