src/Pure/sign.ML
changeset 211 7ab45715c0a6
parent 206 0d624d1ba9cc
child 224 d762f9421933
     1.1 --- a/src/Pure/sign.ML	Tue Jan 04 15:48:38 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Jan 04 17:03:52 1994 +0100
     1.3 @@ -52,6 +52,7 @@
     1.4    val term_of: cterm -> term
     1.5    val typ_of: ctyp -> typ
     1.6    val pretty_term: sg -> term -> Syntax.Pretty.T
     1.7 +val fake_cterm_of: sg -> term -> cterm
     1.8  end;
     1.9  
    1.10  functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    1.11 @@ -294,6 +295,9 @@
    1.12        [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
    1.13      | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
    1.14  
    1.15 +fun fake_cterm_of sign t =
    1.16 +  Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
    1.17 +
    1.18  fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
    1.19  
    1.20  (*Lexing, parsing, polymorphic typechecking of a term.*)