prefer regular print functions over slightly low-level Term.string_of_vname;

--- a/src/Pure/Isar/proof_context.ML	Wed Sep 01 23:03:31 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Sep 01 23:43:45 2010 +0200
@@ -536,14 +536,16 @@
 fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
   (not (abbrev_mode ctxt)) (consts_of ctxt);
 
-fun reject_schematic (Var (xi, _)) =
-      error ("Unbound schematic variable: " ^ Term.string_of_vname xi)
-  | reject_schematic (Abs (_, _, t)) = reject_schematic t
-  | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
-  | reject_schematic _ = ();
+fun expand_binds ctxt =
+  let
+    val Mode {pattern, schematic, ...} = get_mode ctxt;
 
-fun expand_binds ctxt =
-  let val Mode {pattern, schematic, ...} = get_mode ctxt in
+    fun reject_schematic (t as Var _) =
+          error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t)
+      | reject_schematic (Abs (_, _, t)) = reject_schematic t
+      | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
+      | reject_schematic _ = ();
+  in
     if pattern then I
     else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic)
   end;
@@ -576,9 +578,9 @@
     val _ =
       pattern orelse schematic orelse
         T |> Term.exists_subtype
-          (fn TVar (xi, _) =>
+          (fn T as TVar (xi, _) =>
             not (Type_Infer.is_param xi) andalso
-              error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
+              error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T)
           | _ => false)
   in T end;