added fake_cterm_of to speed up rewriting
authornipkow
Tue Jan 04 17:03:52 1994 +0100 (1994-01-04)
changeset 2117ab45715c0a6
parent 210 49497bdf573e
child 212 b2cdb675ef44
added fake_cterm_of to speed up rewriting
src/Pure/drule.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/drule.ML	Tue Jan 04 15:48:38 1994 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Jan 04 17:03:52 1994 +0100
     1.3 @@ -381,7 +381,7 @@
     1.4  
     1.5  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
     1.6  fun goals_conv pred cv sign = 
     1.7 -  let val triv = reflexive o Sign.cterm_of sign
     1.8 +  let val triv = reflexive o Sign.fake_cterm_of sign
     1.9        fun gconv i t =
    1.10          let val (A,B) = Logic.dest_implies t
    1.11  	    val thA = if (pred i) then (cv sign A) else (triv A)
    1.12 @@ -398,7 +398,7 @@
    1.13  
    1.14  (*rewriting conversion*)
    1.15  fun rew_conv prover mss sign t =
    1.16 -  rewrite_cterm mss prover (Sign.cterm_of sign t);
    1.17 +  rewrite_cterm mss prover (Sign.fake_cterm_of sign t);
    1.18  
    1.19  (*Rewrite a theorem*)
    1.20  fun rewrite_rule thms = fconv_rule (rew_conv (K(K None)) (Thm.mss_of thms));
     2.1 --- a/src/Pure/sign.ML	Tue Jan 04 15:48:38 1994 +0100
     2.2 +++ b/src/Pure/sign.ML	Tue Jan 04 17:03:52 1994 +0100
     2.3 @@ -52,6 +52,7 @@
     2.4    val term_of: cterm -> term
     2.5    val typ_of: ctyp -> typ
     2.6    val pretty_term: sg -> term -> Syntax.Pretty.T
     2.7 +val fake_cterm_of: sg -> term -> cterm
     2.8  end;
     2.9  
    2.10  functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    2.11 @@ -294,6 +295,9 @@
    2.12        [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
    2.13      | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
    2.14  
    2.15 +fun fake_cterm_of sign t =
    2.16 +  Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
    2.17 +
    2.18  fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
    2.19  
    2.20  (*Lexing, parsing, polymorphic typechecking of a term.*)