# HG changeset patch
# User haftmann
# Date 1193203196 -7200
# Node ID d813a98a5a367ce679d2b6d46ed7449a55f114d3
# Parent  f3739a8da38fcbb2df8c6f881aefcad306fb18ee
added subclass_rule

diff -r f3739a8da38f -r d813a98a5a36 src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Wed Oct 24 07:19:54 2007 +0200
+++ b/src/Pure/Isar/subclass.ML	Wed Oct 24 07:19:56 2007 +0200
@@ -10,6 +10,7 @@
   val subclass: class -> local_theory -> Proof.state
   val subclass_cmd: xstring -> local_theory -> Proof.state
   val prove_subclass: tactic -> class -> local_theory -> local_theory
+  val subclass_rule: theory -> class * class -> thm
 end;
 
 structure Subclass : SUBCLASS =
@@ -43,6 +44,25 @@
       | NONE => thm;
   in strip end;
 
+fun subclass_rule thy (class1, class2) =
+  let
+    val ctxt = ProofContext.init thy;
+    fun mk_axioms class =
+      let
+        val params = Class.these_params thy [class];
+      in
+        Locale.global_asms_of thy class
+        |> maps snd
+        |> (map o map_aterms) (fn Free (v, _) => (Const o the o AList.lookup (op =) params) v | t => t)
+        |> (map o map_types o map_atyps) (fn TFree _ => TFree (Name.aT, [class1]) | ty => ty)
+        |> map (ObjectLogic.ensure_propT thy)
+      end;
+    val (prems, concls) = pairself mk_axioms (class1, class2);
+  in
+    Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
+      (Locale.intro_locales_tac true ctxt)
+  end;
+
 
 (** subclassing **)