# HG changeset patch
# User wenzelm
# Date 806843612 -7200
# Node ID de2fc8cf9b6aef9fcfc6b5e3f0902de7550eed83
# Parent  d4551b1a6da750da3d7aac176588381c376563e2
minor fix: instance now raises error if witness axioms don't exist;

diff -r d4551b1a6da7 -r de2fc8cf9b6a src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Jul 26 17:35:23 1995 +0200
+++ b/src/Pure/axclass.ML	Thu Jul 27 13:13:32 1995 +0200
@@ -66,7 +66,7 @@
 val is_def = is_equals o #prop o rep_thm;
 
 fun witnesses thy axms thms =
-  get_axioms thy axms @ thms @ filter is_def (map snd (axioms_of thy));
+  map (get_axiom thy) axms @ thms @ filter is_def (map snd (axioms_of thy));