# HG changeset patch
# User wenzelm
# Date 1138384990 -3600
# Node ID d42708f5c1869c1a828f992acd71f2e5622c5fdc
# Parent  93413dcee45b13a21cf766bcad96115251498c40
swapped Toplevel.theory_context;

diff -r 93413dcee45b -r d42708f5c186 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Jan 27 19:03:09 2006 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Jan 27 19:03:10 2006 +0100
@@ -21,9 +21,9 @@
     -> theory -> (string * thm list) list * theory
   val smart_theorems: string -> xstring option ->
     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
-    theory -> theory * Proof.context
+    theory -> Proof.context * theory
   val declare_theorems: xstring option ->
-    (thmref * Attrib.src list) list -> theory -> theory * Proof.context
+    (thmref * Attrib.src list) list -> theory -> Proof.context * theory
   val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     bool -> Proof.state -> Proof.state
   val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
@@ -68,16 +68,16 @@
 
 (* theorems *)
 
-fun present_theorems kind (named_thmss, thy) =
-  conditional (kind <> "" andalso kind <> Drule.internalK) (fn () =>
-    Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss);
+fun present_theorems kind (res, thy) =
+  conditional (kind <> "" andalso kind <> PureThy.internalK) (fn () =>
+    Context.setmp (SOME thy) (Present.results (kind ^ "s")) res);
 
 fun theorems kind args thy = thy
-  |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.attribute thy) args)
+  |> PureThy.note_thmss kind (Attrib.map_facts (Attrib.attribute thy) args)
   |> tap (present_theorems kind);
 
 fun theorems_i kind args =
-  PureThy.note_thmss_i (Drule.kind kind) args
+  PureThy.note_thmss_i kind args
   #> tap (present_theorems kind);
 
 fun apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)];
@@ -86,10 +86,10 @@
 fun smart_theorems kind NONE args thy = thy
       |> theorems kind args
       |> tap (present_theorems kind)
-      |> (fn (_, thy) => (thy, ProofContext.init thy))
+      |> (fn (_, thy) => `ProofContext.init thy)
   | smart_theorems kind (SOME loc) args thy = thy
       |> Locale.note_thmss kind loc args
-      |> tap (present_theorems kind o apsnd fst)
+      |> tap (fn ((_, res), (_, thy')) => present_theorems kind (res, thy'))
       |> #2;
 
 fun declare_theorems opt_loc args =
diff -r 93413dcee45b -r d42708f5c186 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Jan 27 19:03:09 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Jan 27 19:03:10 2006 +0100
@@ -214,8 +214,7 @@
       |> Locale.interpretation (NameSpace.base name_locale, [])
            (Locale.Locale name_locale)
              (map (fn ((c, _), _) => SOME (Sign.intern_const thy c)) cs)
-      |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE)
-      |> swap;
+      |> Proof.global_terminal_proof (Method.Basic (Method.fact ax_axioms), NONE);
     fun print_ctxt ctxt elem = 
       map Pretty.writeln (Element.pretty_ctxt ctxt elem)
   in
@@ -473,7 +472,7 @@
      -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
      -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
       >> (Toplevel.theory_context
-          o (fn f => swap o f) o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
+          o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
 
 val instanceP =
   OuterSyntax.command instanceK "declare instance for operational type class" K.thy_goal