src/Pure/axclass.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18467 bb7b309ac395
     1.1 --- a/src/Pure/axclass.ML	Thu Dec 15 21:51:31 2005 +0100
     1.2 +++ b/src/Pure/axclass.ML	Fri Dec 16 09:00:11 2005 +0100
     1.3 @@ -11,9 +11,9 @@
     1.4    val print_axclasses: theory -> unit
     1.5    val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
     1.6    val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
     1.7 -    theory -> theory * {intro: thm, axioms: thm list}
     1.8 +    theory -> {intro: thm, axioms: thm list} * theory
     1.9    val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
    1.10 -    theory -> theory * {intro: thm, axioms: thm list}
    1.11 +    theory -> {intro: thm, axioms: thm list} * theory
    1.12    val add_classrel_thms: thm list -> theory -> theory
    1.13    val add_arity_thms: thm list -> theory -> theory
    1.14    val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
    1.15 @@ -210,7 +210,7 @@
    1.16        |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
    1.17        ||> Theory.restore_naming class_thy
    1.18        ||> AxclassesData.map (Symtab.update (class, info));
    1.19 -  in (final_thy, {intro = intro, axioms = axioms}) end;
    1.20 +  in ({intro = intro, axioms = axioms}, final_thy) end;
    1.21  
    1.22  in
    1.23  
    1.24 @@ -347,7 +347,7 @@
    1.25    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    1.26      ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    1.27          P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
    1.28 -      >> (Toplevel.theory o (#1 oo uncurry add_axclass)));
    1.29 +      >> (Toplevel.theory o (snd oo uncurry add_axclass)));
    1.30  
    1.31  val instanceP =
    1.32    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal