src/HOL/List.ML
changeset 9108 9fff97d29837
parent 9014 4382883421ec
child 9187 68ecc04785f1
--- a/src/HOL/List.ML	Thu Jun 22 11:37:13 2000 +0200
+++ b/src/HOL/List.ML	Thu Jun 22 23:04:34 2000 +0200
@@ -32,7 +32,7 @@
 by (REPEAT (ares_tac basic_monos 1));
 qed "lists_mono";
 
-val listsE = lists.mk_cases "x#l : lists A";
+bind_thm ("listsE", lists.mk_cases "x#l : lists A");
 AddSEs [listsE];
 AddSIs lists.intrs;