# HG changeset patch
# User nipkow
# Date 935393765 -7200
# Node ID 768fab6dae742c7edf21d8745ed6676e8f011997
# Parent  ece660815e03b5ab0de08649578b2833efb2e6a2
Corrected two busg in the simplifier.

diff -r ece660815e03 -r 768fab6dae74 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Aug 22 21:14:44 1999 +0200
+++ b/src/Pure/term.ML	Mon Aug 23 09:36:05 1999 +0200
@@ -37,6 +37,7 @@
     $ of term * term
   exception TYPE of string * typ list * term list
   exception TERM of string * term list
+  val is_Bound: term -> bool
   val is_Const: term -> bool
   val is_Free: term -> bool
   val is_Var: term -> bool
@@ -241,6 +242,9 @@
 
 (** Discriminators **)
 
+fun is_Bound (Bound _) = true
+  | is_Bound _         = false;
+
 fun is_Const (Const _) = true
   | is_Const _ = false;
 
diff -r ece660815e03 -r 768fab6dae74 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Aug 22 21:14:44 1999 +0200
+++ b/src/Pure/thm.ML	Mon Aug 23 09:36:05 1999 +0200
@@ -1809,10 +1809,6 @@
 
 (* add_congs *)
 
-(*FIXME -> term.ML *)
-fun is_Bound (Bound _) = true
-fun is_Bound _         = false;
-
 fun is_full_cong_prems [] varpairs = null varpairs
   | is_full_cong_prems (p::prems) varpairs =
     (case Logic.strip_assums_concl p of
@@ -1821,7 +1817,7 @@
          in is_Var x  andalso  forall is_Bound xs  andalso
             null(findrep(xs))  andalso xs=ys andalso
             (x,y) mem varpairs andalso
-            is_full_cong_prems (p::prems) (varpairs\(x,y))
+            is_full_cong_prems prems (varpairs\(x,y))
          end
      | _ => false);