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