# HG changeset patch
# User wenzelm
# Date 1440761826 -7200
# Node ID c2155072c2f48b9cd6410e19514a33b234d9551a
# Parent  58e41aa1c36db45dc0e05da3b467481d5115b4fc
tuned signature;

diff -r 58e41aa1c36d -r c2155072c2f4 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 28 13:36:33 2015 +0200
+++ b/src/Pure/thm.ML	Fri Aug 28 13:37:06 2015 +0200
@@ -52,14 +52,6 @@
   val first_order_match: cterm * cterm ->
     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   (*theorems*)
-  val rep_thm: thm ->
-   {thy: theory,
-    tags: Properties.T,
-    maxidx: int,
-    shyps: sort Ord_List.T,
-    hyps: term Ord_List.T,
-    tpairs: (term * term) list,
-    prop: term}
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
   val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
   val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a