# HG changeset patch
# User wenzelm
# Date 895224956 -7200
# Node ID 683eae4b5d0f53c2e62acd4bdcd20e444fadc214
# Parent  c85b339accfe018c01e5f411c4fc5b581153bbd5
witnesses: lookup stored thms instead of axioms;

diff -r c85b339accfe -r 683eae4b5d0f src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri May 15 11:34:49 1998 +0200
+++ b/src/Pure/axclass.ML	Fri May 15 11:35:56 1998 +0200
@@ -60,8 +60,8 @@
 
 val is_def = Logic.is_equals o #prop o rep_thm;
 
-fun witnesses thy axms thms =
-  map (get_axiom thy) axms @ thms @ filter is_def (map snd (axioms_of thy));
+fun witnesses thy names thms =
+  flat (map (PureThy.get_thms thy) names) @ thms @ filter is_def (map snd (axioms_of thy));
 
 
 
@@ -287,7 +287,7 @@
 fun intrn_classrel sg c1_c2 =
   pairself (Sign.intern_class sg) c1_c2;
 
-fun ext_inst_subclass int raw_c1_c2 axms thms usr_tac thy =
+fun ext_inst_subclass int raw_c1_c2 names thms usr_tac thy =
   let
     val c1_c2 =
       if int then intrn_classrel (sign_of thy) raw_c1_c2
@@ -296,20 +296,20 @@
     writeln ("Proving class inclusion " ^
       quote (Sign.str_of_classrel (sign_of thy) c1_c2) ^ " ...");
     add_classrel_thms
-      [prove_subclass thy c1_c2 (witnesses thy axms thms) usr_tac] thy
+      [prove_subclass thy c1_c2 (witnesses thy names thms) usr_tac] thy
   end;
 
 
 fun intrn_arity sg intrn (t, Ss, x) =
   (Sign.intern_tycon sg t, map (Sign.intern_sort sg) Ss, intrn sg x);
 
-fun ext_inst_arity int (raw_t, raw_Ss, raw_cs) axms thms usr_tac thy =
+fun ext_inst_arity int (raw_t, raw_Ss, raw_cs) names thms usr_tac thy =
   let
     val sign = sign_of thy;
     val (t, Ss, cs) =
       if int then intrn_arity sign Sign.intern_sort (raw_t, raw_Ss, raw_cs)
       else (raw_t, raw_Ss, raw_cs);
-    val wthms = witnesses thy axms thms;
+    val wthms = witnesses thy names thms;
     fun prove c =
      (writeln ("Proving type arity " ^
         quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ...");