# 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