summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Thu, 21 Oct 1993 14:38:06 +0100 | |

changeset 61 | f8c1922b78e3 |

parent 60 | 379872528c16 |

child 62 | facfff975d1a |

Pure/term/fastype_of1: renamed from fastype_of
Pure/term/fastype_of: new, takes only one argument (like type_of)
Pure/Syntax/printer/is_prop: now calls fastype_of1
Pure/pattern: now calls new fastype_of in three places
Pure/logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
So it no longer checks t properly -- but it never checked u anyway, and all
existing calls are derived from certified terms...

src/Pure/term.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/term.ML Sun Oct 17 18:03:47 1993 +0100 +++ b/src/Pure/term.ML Thu Oct 21 14:38:06 1993 +0100 @@ -130,19 +130,21 @@ [T,U], [f$u]) end; - fun type_of t : typ = type_of1 ([],t); (*Determines the type of a term, with minimal checking*) -fun fastype_of(Ts, f$u) = (case fastype_of(Ts,f) of +fun fastype_of1 (Ts, f$u) = + (case fastype_of1 (Ts,f) of Type("fun",[_,T]) => T | _ => raise TERM("fastype_of: expected function type", [f$u])) - | fastype_of(_, Const (_,T)) = T - | fastype_of(_, Free (_,T)) = T - | fastype_of(Ts, Bound i) = (nth_elem(i,Ts) + | fastype_of1 (_, Const (_,T)) = T + | fastype_of1 (_, Free (_,T)) = T + | fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts) handle LIST _ => raise TERM("fastype_of: Bound", [Bound i])) - | fastype_of(_, Var (_,T)) = T - | fastype_of(Ts, Abs (_,T,u)) = T --> fastype_of(T::Ts, u); + | fastype_of1 (_, Var (_,T)) = T + | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u); + +fun fastype_of t : typ = fastype_of1 ([],t); (* maps (x1,...,xn)t to t *)