src/Pure/sign.ML
changeset 211 7ab45715c0a6
parent 206 0d624d1ba9cc
child 224 d762f9421933
--- 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.*)