--- 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.*)