author | haftmann |
Fri, 17 Dec 2010 18:32:40 +0100 | |
changeset 41248 | bb28bf635202 |
parent 41247 | c5cb19ecbd41 |
child 41252 | 4ae674714876 |
src/Pure/conv.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/conv.ML Fri Dec 17 18:24:44 2010 +0100 +++ b/src/Pure/conv.ML Fri Dec 17 18:32:40 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;