parse_term: invoke full Syntax.check_term, not just standard_infer_types;

--- a/src/Pure/Isar/proof_context.ML	Wed Oct 24 07:19:57 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Oct 24 17:17:43 2007 +0200
@@ -563,6 +563,8 @@
 
 (* type checking/inference *)
 
+local
+
 fun standard_infer_types ctxt ts =
   let val Mode {pattern, ...} = get_mode ctxt in
     TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
@@ -572,8 +574,6 @@
     handle TYPE (msg, _, _) => error msg
   end;
 
-local
-
 fun standard_typ_check ctxt =
   map (cert_typ_mode (Type.get_mode ctxt) ctxt) #>
   map (prepare_patternT ctxt);
@@ -647,13 +647,12 @@
 fun parse_term T ctxt str =
   let
     val thy = theory_of ctxt;
-    val infer = singleton (standard_infer_types (Type.set_mode Type.mode_default ctxt)) o
-      TypeInfer.constrain T;
-    fun check t = Exn.Result (infer t) handle ERROR msg => Exn.Exn (ERROR msg);
+    val (T', _) = TypeInfer.paramify_dummies T 0;
+    fun check t = Exn.Result (Syntax.check_term ctxt (TypeInfer.constrain T' t))
+      handle ERROR msg => Exn.Exn (ERROR msg);
     val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
     val read = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort
-      map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt)
-      ((#1 (TypeInfer.paramify_dummies T 0)));
+      map_const map_free map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T';
   in read str end;