src/Pure/thm.ML
changeset 46475 22eaaf4f00a3
parent 46255 6fae74ee591a
child 46497 89ccf66aa73d
--- 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