src/Pure/Isar/element.ML
changeset 19843 67cb97e856ff
parent 19808 396dd23c54ef
child 19866 d47f32a4964a
     1.1 --- a/src/Pure/Isar/element.ML	Sun Jun 11 21:59:21 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sun Jun 11 21:59:23 2006 +0200
     1.3 @@ -60,6 +60,7 @@
     1.4    val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
     1.5    val satisfy_thm: witness list -> thm -> thm
     1.6    val satisfy_witness: witness list -> witness -> witness
     1.7 +  val satisfy_ctxt: witness list -> context_i -> context_i
     1.8  end;
     1.9  
    1.10  structure Element: ELEMENT =
    1.11 @@ -444,4 +445,6 @@
    1.12  
    1.13  fun satisfy_witness witns = map_witness (apsnd (satisfy_thm witns));
    1.14  
    1.15 +fun satisfy_ctxt witns = map_ctxt_values I I (satisfy_thm witns);
    1.16 +
    1.17  end;