# HG changeset patch
# User wenzelm
# Date 1120050805 -7200
# Node ID e64fb2cf50cb2abc98ffcfcd706fdc9550840147
# Parent  5d73fbf4eb1e93e71e1cdc4a48455c85f66483e4
added implies_intr_hyps (from thm.ML);

diff -r 5d73fbf4eb1e -r e64fb2cf50cb src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jun 29 15:13:23 2005 +0200
+++ b/src/Pure/drule.ML	Wed Jun 29 15:13:25 2005 +0200
@@ -40,6 +40,7 @@
   val instantiate       :
     (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   val zero_var_indexes  : thm -> thm
+  val implies_intr_hyps : thm -> thm
   val standard          : thm -> thm
   val standard'         : thm -> thm
   val rotate_prems      : int -> thm -> thm
@@ -438,6 +439,10 @@
 (** Standard form of object-rule: no hypotheses, flexflex constraints,
     Frees, or outer quantifiers; all generality expressed by Vars of index 0.**)
 
+(*Discharge all hypotheses.*)
+fun implies_intr_hyps th =
+  fold Thm.implies_intr (#hyps (Thm.crep_thm th)) th;
+
 (*Squash a theorem's flexflex constraints provided it can be done uniquely.
   This step can lose information.*)
 fun flexflex_unique th =
@@ -641,7 +646,7 @@
 
 val symmetric_thm =
   let val xy = read_prop "x == y"
-  in store_standard_thm_open "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
+  in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end;
 
 val transitive_thm =
   let val xy = read_prop "x == y"