more efficient prepare_sorts -- bypass encoded positions;

--- a/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 22:54:15 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 23:30:50 2011 +0100
@@ -809,9 +809,13 @@
     val get_sort = Proof_Context.get_sort ctxt env;
   in
     (map o map_atyps)
-      (fn TFree (x, _) => TFree (x, get_sort (x, ~1))
-        | TVar (xi, _) => TVar (xi, get_sort xi)
-        | T => T) tys
+      (fn T =>
+        if Term_Position.is_positionT T then T
+        else
+          (case T of
+            TFree (x, _) => TFree (x, get_sort (x, ~1))
+          | TVar (xi, _) => TVar (xi, get_sort xi)
+          | _ => T)) tys
   end;
 
 in
@@ -823,10 +827,11 @@
 
 fun check_terms ctxt raw_ts =
   let
-    val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts;
+    val (ts, ps) = raw_ts
+      |> Term.burrow_types (prepare_sorts ctxt)
+      |> Type_Infer_Context.prepare_positions ctxt;
     val tys = map (Logic.mk_type o snd) ps;
-    val (ts', tys') =
-      Term.burrow_types (prepare_sorts ctxt) ts @ tys
+    val (ts', tys') = ts @ tys
       |> apply_term_check ctxt
       |> chop (length ts);
     val _ =

--- a/src/Pure/Syntax/term_position.ML	Thu Nov 10 22:54:15 2011 +0100
+++ b/src/Pure/Syntax/term_position.ML	Thu Nov 10 23:30:50 2011 +0100
@@ -12,6 +12,7 @@
   val decode_position: term -> (Position.T * typ) option
   val decode_positionT: typ -> Position.T option
   val is_position: term -> bool
+  val is_positionT: typ -> bool
   val strip_positions: term -> term
 end;
 
@@ -50,6 +51,7 @@
   | decode_positionT _ = NONE;
 
 val is_position = is_some o decode_position;
+val is_positionT = is_some o decode_positionT;
 
 fun strip_positions ((t as Const (c, _)) $ u $ v) =
       if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v