# HG changeset patch
# User wenzelm
# Date 1085167462 -7200
# Node ID 724ce6e574e34440e15a62cf09a9543b2a1d7ad6
# Parent  24a7bc97a27a4e5f853ff6dc9c07d72d2d7bb5b3
adapted tsig interface;

diff -r 24a7bc97a27a -r 724ce6e574e3 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri May 21 21:23:37 2004 +0200
+++ b/src/Pure/pattern.ML	Fri May 21 21:24:22 2004 +0200
@@ -15,39 +15,32 @@
 infix aeconv;
 
 signature PATTERN =
-  sig
-  type type_sig
-  type sg
-  type env
+sig
   val trace_unify_fail  : bool ref
   val aeconv            : term * term -> bool
   val eta_contract      : term -> term
   val eta_long          : typ list -> term -> term
   val beta_eta_contract : term -> term
   val eta_contract_atom : term -> term
-  val match             : type_sig -> term * term
+  val match             : Type.tsig -> term * term
                           -> (indexname*typ)list * (indexname*term)list
-  val first_order_match : type_sig -> term * term
+  val first_order_match : Type.tsig -> term * term
                           -> (indexname*typ)list * (indexname*term)list
-  val matches           : type_sig -> term * term -> bool
-  val matches_subterm   : type_sig -> term * term -> bool
-  val unify             : sg * env * (term * term)list -> env
+  val matches           : Type.tsig -> term * term -> bool
+  val matches_subterm   : Type.tsig -> term * term -> bool
+  val unify             : Sign.sg * Envir.env * (term * term)list -> Envir.env
   val first_order       : term -> bool
   val pattern           : term -> bool
-  val rewrite_term      : type_sig -> (term * term) list -> (term -> term option) list
+  val rewrite_term      : Type.tsig -> (term * term) list -> (term -> term option) list
                           -> term -> term
   exception Unif
   exception MATCH
   exception Pattern
-  end;
+end;
 
 structure Pattern : PATTERN =
 struct
 
-type type_sig = Type.type_sig
-type sg = Sign.sg
-type env = Envir.env
-
 exception Unif;
 exception Pattern;
 
@@ -238,7 +231,7 @@
                  end;
   in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
 
-val tsgr = ref(Type.tsig0);
+val tsgr = ref(Type.empty_tsig);
 
 fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env
@@ -296,16 +289,16 @@
 fun eta_contract t =
   let
     exception SAME;
-    fun eta (Abs (a, T, body)) = 
+    fun eta (Abs (a, T, body)) =
       ((case eta body of
-          body' as (f $ Bound 0) => 
-	    if loose_bvar1 (f, 0) then Abs(a, T, body')
-	    else incr_boundvars ~1 f
+          body' as (f $ Bound 0) =>
+            if loose_bvar1 (f, 0) then Abs(a, T, body')
+            else incr_boundvars ~1 f
         | body' => Abs (a, T, body')) handle SAME =>
        (case body of
-          (f $ Bound 0) => 
-	    if loose_bvar1 (f, 0) then raise SAME
-	    else incr_boundvars ~1 f
+          (f $ Bound 0) =>
+            if loose_bvar1 (f, 0) then raise SAME
+            else incr_boundvars ~1 f
         | _ => raise SAME))
       | eta (f $ t) =
           (let val f' = eta f
@@ -333,7 +326,7 @@
 fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
   | eta_long Ts t = (case strip_comb t of
       (Abs _, _) => eta_long Ts (Envir.beta_norm t)
-    | (u, ts) => 
+    | (u, ts) =>
       let
         val Us = binder_types (fastype_of1 (Ts, t));
         val i = length Us
@@ -524,7 +517,7 @@
             Abs (_, _, body) =>
               let val tm' = subst_bound (tm2, body)
               in Some (if_none (rew2 skel0 tm') tm') end
-          | _ => 
+          | _ =>
             let val (skel1, skel2) = (case skel of
                 skel1 $ skel2 => (skel1, skel2)
               | _ => (skel0, skel0))
diff -r 24a7bc97a27a -r 724ce6e574e3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri May 21 21:23:37 2004 +0200
+++ b/src/Pure/proofterm.ML	Fri May 21 21:24:22 2004 +0200
@@ -104,7 +104,7 @@
   val add_prf_rrules : (proof * proof) list -> theory -> theory
   val add_prf_rprocs : (string * (Term.typ list -> proof -> proof option)) list ->
     theory -> theory
-  val rewrite_proof : Type.type_sig -> (proof * proof) list *
+  val rewrite_proof : Type.tsig -> (proof * proof) list *
     (string * (typ list -> proof -> proof option)) list -> proof -> proof
   val rewrite_proof_notypes : (proof * proof) list *
     (string * (typ list -> proof -> proof option)) list -> proof -> proof