# HG changeset patch
# User wenzelm
# Date 1006618907 -3600
# Node ID 2ef49890aede28ec66d756298ce7a403c240cc01
# Parent  ce14a4faededef7cf0020950bb0794e1697e5006
fixed SML/NJ error (!?);

diff -r ce14a4faeded -r 2ef49890aede src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Nov 24 17:02:39 2001 +0100
+++ b/src/Pure/proofterm.ML	Sat Nov 24 17:21:47 2001 +0100
@@ -118,8 +118,8 @@
    PBound of int
  | Abst of string * typ option * proof
  | AbsP of string * term option * proof
- | op % of proof * term option
- | op %% of proof * proof
+ | % of proof * term option
+ | %% of proof * proof
  | Hyp of term
  | PThm of (string * (string * string list) list) * proof * term * typ list option
  | PAxm of string * term * typ list option
@@ -915,8 +915,6 @@
                    ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
                  else raise PMatch
             | _ => raise PMatch)
-      | mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) =
-          ((ixn, prf) :: pinst, tinst)
       | mtch Ts i j inst (prf1 % opt1, prf2 % opt2) =
           optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2)
       | mtch Ts i j inst (prf1 %% prf2, prf1' %% prf2') =