# HG changeset patch
# User wenzelm
# Date 1329254521 -3600
# Node ID 22eaaf4f00a39f1ec4f302989a750d69c068cb36
# Parent  7e6be8270ddb828e20a1e595c610ca15cb10ef88
tuned signature;

diff -r 7e6be8270ddb -r 22eaaf4f00a3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Feb 14 21:59:10 2012 +0100
+++ b/src/Pure/thm.ML	Tue Feb 14 22:22:01 2012 +0100
@@ -136,7 +136,6 @@
   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
-  val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
   val assumption: int -> thm -> thm Seq.seq