# HG changeset patch
# User wenzelm
# Date 1191942648 -7200
# Node ID 9f5d60fe908650505027c4a6c417216acfd4cba8
# Parent  5471b164813bba7909e85f15edfa22f701836d05
renamed AxClass.get_definition to AxClass.get_info (again);
simplified goal setup using Proof.theorem_i;

diff -r 5471b164813b -r 9f5d60fe9086 src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Tue Oct 09 17:10:46 2007 +0200
+++ b/src/Pure/Isar/subclass.ML	Tue Oct 09 17:10:48 2007 +0200
@@ -82,8 +82,8 @@
           |> filter_out (fn class' => Sign.subsort thy ([sub], [class']));
         fun instance_subclass (class1, class2) thy  =
           let
-            val ax = #axioms (AxClass.get_definition thy class1);
-            val intro = #intro (AxClass.get_definition thy class2)
+            val ax = #axioms (AxClass.get_info thy class1);
+            val intro = #intro (AxClass.get_info thy class2)
               |> Drule.instantiate' [SOME (Thm.ctyp_of thy
                   (TVar ((Name.aT, 0), [class1])))] [];
             val thm =
@@ -96,9 +96,9 @@
       in
         thy |> fold_rev (curry instance_subclass sub) classes
       end;
-    fun after_qed thmss =
+    fun after_qed [thms] =
       let
-        val thm = Conjunction.intr_balanced (the_single thmss);;
+        val thm = Conjunction.intr_balanced thms;
         val interp = export thm;
       in
         LocalTheory.theory (prove_classrel interp
@@ -106,11 +106,8 @@
              I (loc_name, loc_expr))
         (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*)
       end;
-    val goal = Element.Shows
-      [(("", []), map (rpair []) (mk_subclass_rule lthy sup))];
-  in 
-    Specification.theorem_i Thm.internalK NONE after_qed ("", []) [] goal true lthy
-  end;
+
+  in Proof.theorem_i NONE after_qed [map (rpair []) (mk_subclass_rule lthy sup)] lthy end;
 
 in