src/Pure/axclass.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18467 bb7b309ac395
--- a/src/Pure/axclass.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/axclass.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -11,9 +11,9 @@
   val print_axclasses: theory -> unit
   val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
   val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
-    theory -> theory * {intro: thm, axioms: thm list}
+    theory -> {intro: thm, axioms: thm list} * theory
   val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
-    theory -> theory * {intro: thm, axioms: thm list}
+    theory -> {intro: thm, axioms: thm list} * theory
   val add_classrel_thms: thm list -> theory -> theory
   val add_arity_thms: thm list -> theory -> theory
   val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
@@ -210,7 +210,7 @@
       |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
       ||> Theory.restore_naming class_thy
       ||> AxclassesData.map (Symtab.update (class, info));
-  in (final_thy, {intro = intro, axioms = axioms}) end;
+  in ({intro = intro, axioms = axioms}, final_thy) end;
 
 in
 
@@ -347,7 +347,7 @@
   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
         P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
-      >> (Toplevel.theory o (#1 oo uncurry add_axclass)));
+      >> (Toplevel.theory o (snd oo uncurry add_axclass)));
 
 val instanceP =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal