# HG changeset patch
# User dixon
# Date 1150563492 -7200
# Node ID 9e5d0df75c98e56da8d47700c424d4b1d19a9f30
# Parent  781046997aab0cfebf9606976cfbff7f714ae890
added interface for making term contexts.

diff -r 781046997aab -r 9e5d0df75c98 src/Provers/IsaPlanner/zipper.ML
--- a/src/Provers/IsaPlanner/zipper.ML	Fri Jun 16 09:08:34 2006 +0200
+++ b/src/Provers/IsaPlanner/zipper.ML	Sat Jun 17 18:58:12 2006 +0200
@@ -58,10 +58,16 @@
 signature TRM_CTXT =
 sig
   structure D : TRM_CTXT_DATA
-  type T = D.dtrm list
+  type T = D.dtrm list;
+
+  val empty : T;
+  val is_empty : T -> bool;
 
-  val empty : T
-  val is_empty : T -> bool
+  val add_abs : D.Trm.aname * D.Trm.typ -> T -> T;
+  val add_appl : D.Trm.T -> T -> T;
+  val add_appr : D.Trm.T -> T -> T;
+
+  val add_dtrm : D.dtrm -> T -> T;
 
   val eq_path : T * T -> bool
 
@@ -188,6 +194,12 @@
   val empty = [];
   val is_empty = List.null;
 
+  fun add_abs d l = (D.Abs d) :: l;
+  fun add_appl d l = (D.AppL d) :: l;
+  fun add_appr d l = (D.AppR d) :: l;
+
+  fun add_dtrm d l = d::l;
+
   fun eq_path ([], []) = true
     | eq_path ([], _::_) = false
     | eq_path ( _::_, []) = false