# HG changeset patch
# User wenzelm
# Date 1150055963 -7200
# Node ID 67cb97e856ff2a6cfe27c64d4bb7d6938ec91f1d
# Parent  04120bdac80e305c762df637167fbaa72f0d429b
added satisfy_ctxt;

diff -r 04120bdac80e -r 67cb97e856ff src/Pure/Isar/element.ML
--- 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;