# HG changeset patch
# User wenzelm
# Date 1011730755 -3600
# Node ID 37202992c7e36ab37bdfaba5d1a4eb5adfcb8336
# Parent  e5bec326893227752ac77e729c1f6bb57ecd9cee
qualified_result replaces qualified;

diff -r e5bec3268932 -r 37202992c7e3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jan 22 21:18:36 2002 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Jan 22 21:19:15 2002 +0100
@@ -77,7 +77,7 @@
   val get_thms: context -> string -> thm list
   val get_thms_closure: context -> string -> thm list
   val cond_extern: context -> string -> xstring
-  val qualified: (context -> context) -> context -> context
+  val qualified_result: (context -> context * 'a) -> context -> context * 'a
   val put_thm: string * thm -> context -> context
   val put_thms: string * thm list -> context -> context
   val put_thmss: (string * thm list) list -> context -> context
@@ -94,10 +94,10 @@
   val export_def: exporter
   val assume: exporter
     -> ((string * context attribute list) * (string * (string list * string list)) list) list
-    -> context -> context * (string * thm list) list
+    -> context -> context * (bstring * thm list) list
   val assume_i: exporter
     -> ((string * context attribute list) * (term * (term list * term list)) list) list
-    -> context -> context * (string * thm list) list
+    -> context -> context * (bstring * thm list) list
   val read_vars: context * (string list * string option) -> context * (string list * typ option)
   val cert_vars: context * (string list * typ option) -> context * (string list * typ option)
   val fix: (string list * string option) list -> context -> context
@@ -933,8 +933,8 @@
 fun set_qual q = map_context (fn (thy, syntax, data, asms, binds, (_, space, tab), cases, defs) =>
   (thy, syntax, data, asms, binds, (q, space, tab), cases, defs));
 
-fun qualified f (ctxt as Context {thms, ...}) =
-  ctxt |> set_qual true |> f |> set_qual (#1 thms);
+fun qualified_result f (ctxt as Context {thms, ...}) =
+  ctxt |> set_qual true |> f |>> set_qual (#1 thms);
 
 
 (* put_thm(s) *)