# HG changeset patch
# User wenzelm
# Date 791209886 -3600
# Node ID 9af08725600bad62cf1ddc893a42d9dd97ab3a3a
# Parent  190f89d8563c06469b334cbe5be0590be395101e
instance: now automatically includes defs of current thy node as witnesses;

diff -r 190f89d8563c -r 9af08725600b src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Jan 27 13:29:44 1995 +0100
+++ b/src/Pure/axclass.ML	Fri Jan 27 13:31:26 1995 +0100
@@ -56,13 +56,18 @@
 fun aT S = TFree ("'a", S);
 
 
-(* get axioms *)
+(* get axioms and theorems *)
 
 fun get_ax thy name =
   Some (get_axiom thy name) handle THEORY _ => None;
 
 val get_axioms = mapfilter o get_ax;
 
+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));
+
 
 
 (** abstract syntax operations **)
@@ -245,8 +250,6 @@
   (2) rewrite goals using user supplied definitions
   (3) repeatedly resolve goals with user supplied non-definitions*)
 
-val is_def = is_equals o #prop o rep_thm;
-
 fun axclass_tac thy thms =
   TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN
   TRY (rewrite_goals_tac (filter is_def thms)) THEN
@@ -285,19 +288,20 @@
 
 (** add proved subclass relations and arities **)
 
+
+
 fun add_inst_subclass (c1, c2) axms thms usr_tac thy =
   add_classrel_thms
-  [prove_subclass thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy;
+  [prove_subclass thy (c1, c2) (witnesses thy axms thms) usr_tac] thy;
 
 fun add_inst_arity (t, ss, cs) axms thms usr_tac thy =
   let
-    val usr_thms = get_axioms thy axms @ thms;
+    val wthms = witnesses thy axms thms;
     fun prove c =
-      prove_arity thy (t, ss, c) usr_thms usr_tac;
+      prove_arity thy (t, ss, c) wthms usr_tac;
   in
     add_arity_thms (map prove cs) thy
   end;
 
 
 end;
-