# HG changeset patch
# User nipkow
# Date 757699432 -3600
# Node ID 7ab45715c0a6d7624fe19f9514aaecd3e6cb9dce
# Parent  49497bdf573e15096e6ad744bde5a681b7c0c5cc
added fake_cterm_of to speed up rewriting

diff -r 49497bdf573e -r 7ab45715c0a6 src/Pure/drule.ML
--- 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));
diff -r 49497bdf573e -r 7ab45715c0a6 src/Pure/sign.ML
--- 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.*)