--- a/src/Pure/drule.ML Tue Jan 04 15:48:38 1994 +0100
+++ b/src/Pure/drule.ML Tue Jan 04 17:03:52 1994 +0100
@@ -381,7 +381,7 @@
(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
fun goals_conv pred cv sign =
- let val triv = reflexive o Sign.cterm_of sign
+ let val triv = reflexive o Sign.fake_cterm_of sign
fun gconv i t =
let val (A,B) = Logic.dest_implies t
val thA = if (pred i) then (cv sign A) else (triv A)
@@ -398,7 +398,7 @@
(*rewriting conversion*)
fun rew_conv prover mss sign t =
- rewrite_cterm mss prover (Sign.cterm_of sign t);
+ rewrite_cterm mss prover (Sign.fake_cterm_of sign t);
(*Rewrite a theorem*)
fun rewrite_rule thms = fconv_rule (rew_conv (K(K None)) (Thm.mss_of thms));
--- a/src/Pure/sign.ML Tue Jan 04 15:48:38 1994 +0100
+++ b/src/Pure/sign.ML Tue Jan 04 17:03:52 1994 +0100
@@ -52,6 +52,7 @@
val term_of: cterm -> term
val typ_of: ctyp -> typ
val pretty_term: sg -> term -> Syntax.Pretty.T
+val fake_cterm_of: sg -> term -> cterm
end;
functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
@@ -294,6 +295,9 @@
[] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
| errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
+fun fake_cterm_of sign t =
+ Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
+
fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
(*Lexing, parsing, polymorphic typechecking of a term.*)