# HG changeset patch
# User wenzelm
# Date 1440755526 -7200
# Node ID 9c28a4feebd18cee84fafb3bf6ba4a93e548f094
# Parent  0e273cbec33fb3a2c31bfa55719ca8bacd394988
tuned;

diff -r 0e273cbec33f -r 9c28a4feebd1 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Fri Aug 28 11:13:22 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML	Fri Aug 28 11:52:06 2015 +0200
@@ -918,9 +918,8 @@
 fun chyps thm = map Dcterm.drop_prop (Thm.chyps_of thm);
 
 fun dest_thm thm =
-  let val {prop,hyps,...} = Thm.rep_thm thm
-  in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end
-  handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
+  (map HOLogic.dest_Trueprop (Thm.hyps_of thm), HOLogic.dest_Trueprop (Thm.prop_of thm))
+    handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
 
 
 (* Inference rules *)
@@ -1225,19 +1224,6 @@
        blist' th
   end;
 
-(*---------------------------------------------------------------------------
- *  Faster version, that fails for some as yet unknown reason
- * fun IT_EXISTS blist th =
- *    let val {thy,...} = rep_thm th
- *        val tych = cterm_of thy
- *        fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
- *   in
- *  fold (fn (b as (r1,r2), thm) =>
- *  EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
- *           r1) thm)  blist th
- *   end;
- *---------------------------------------------------------------------------*)
-
 (*----------------------------------------------------------------------------
  *        Rewriting
  *---------------------------------------------------------------------------*)