# HG changeset patch
# User wenzelm
# Date 807290421 -7200
# Node ID f96a04c6b352e8aee62af3b6f455bf237f35d8cf
# Parent  a2f2360ce1c8c342802e12f11ef88d073dfb8439
modified prep_thm_axm to handle shyps;
fixed class_axms: class_trivs *first*;
improved axclass_tac: now also handles object rules as witnesses;

diff -r a2f2360ce1c8 -r f96a04c6b352 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Aug 01 17:19:17 1995 +0200
+++ b/src/Pure/axclass.ML	Tue Aug 01 17:20:21 1995 +0200
@@ -121,11 +121,11 @@
   let
     fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]);
 
-    val {sign, hyps, prop, ...} = rep_thm thm;
+    val {sign, shyps, hyps, prop, ...} = rep_thm thm;
   in
     if not (Sign.subsig (sign, sign_of thy)) then
       err "theorem not of same theory"
-    else if not (null hyps) then
+    else if not (null shyps) orelse not (null hyps) then
       err "theorem may not contain hypotheses"
     else prop
   end;
@@ -238,22 +238,27 @@
     val classes = Sign.classes (sign_of thy);
     val intros = map (fn c => c ^ "I") classes;
   in
-    get_axioms thy intros @
-    map (class_triv thy) classes
+    map (class_triv thy) classes @
+    get_axioms thy intros
   end;
 
 
 (* axclass_tac *)
 
 (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
-      try "cI" axioms first and use class_triv as last resort
+      try class_trivs first, then "cI" axioms
   (2) rewrite goals using user supplied definitions
   (3) repeatedly resolve goals with user supplied non-definitions*)
 
 fun axclass_tac thy thms =
-  TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN
-  TRY (rewrite_goals_tac (filter is_def thms)) THEN
-  TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms)));
+  let
+    val defs = filter is_def thms;
+    val non_defs = filter_out is_def thms;
+  in
+    TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN
+    TRY (rewrite_goals_tac defs) THEN
+    TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
+  end;
 
 
 (* provers *)
@@ -288,8 +293,6 @@
 
 (** 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) (witnesses thy axms thms) usr_tac] thy;