tuned signature;
authorwenzelm
Tue, 14 Feb 2012 22:22:01 +0100
changeset 46475 22eaaf4f00a3
parent 46474 7e6be8270ddb
child 46476 dac966e4e51d
tuned signature;
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