author | wenzelm |
Fri, 17 Dec 2010 18:38:33 +0100 | |
changeset 41252 | 4ae674714876 |
parent 41248 | bb28bf635202 (diff) |
parent 41251 | 1e6d86821718 (current diff) |
child 41253 | 42f24340ae53 |
child 41257 | a47133170dd0 |
src/Pure/meta_simplifier.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/conv.ML Fri Dec 17 18:33:35 2010 +0100 +++ b/src/Pure/conv.ML Fri Dec 17 18:38:33 2010 +0100 @@ -48,7 +48,6 @@ val concl_conv: int -> conv -> conv val fconv_rule: conv -> thm -> thm val gconv_rule: conv -> int -> thm -> thm - val tap_thy: (theory -> conv) -> conv end; structure Conv: CONV = @@ -212,9 +211,6 @@ end | NONE => raise THM ("gconv_rule", i, [th])); - -fun tap_thy conv ct = conv (Thm.theory_of_cterm ct) ct; - end; structure Basic_Conv: BASIC_CONV = Conv;