# HG changeset patch
# User lcp
# Date 751210686 -3600
# Node ID f8c1922b78e31b174ee0bd272d158907e995e0a3
# Parent  379872528c169d0eaca5db3d04de48479b409b78
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...

diff -r 379872528c16 -r f8c1922b78e3 src/Pure/term.ML
--- 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  *)