added satisfy_ctxt;

--- a/src/Pure/Isar/element.ML	Sun Jun 11 21:59:21 2006 +0200
+++ b/src/Pure/Isar/element.ML	Sun Jun 11 21:59:23 2006 +0200
@@ -60,6 +60,7 @@
   val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
   val satisfy_thm: witness list -> thm -> thm
   val satisfy_witness: witness list -> witness -> witness
+  val satisfy_ctxt: witness list -> context_i -> context_i
 end;
 
 structure Element: ELEMENT =
@@ -444,4 +445,6 @@
 
 fun satisfy_witness witns = map_witness (apsnd (satisfy_thm witns));
 
+fun satisfy_ctxt witns = map_ctxt_values I I (satisfy_thm witns);
+
 end;