--- 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;