tuned;

--- a/src/Pure/Isar/proof_context.ML	Sun Jun 14 12:48:32 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 14 14:59:39 2015 +0200
@@ -1034,14 +1034,14 @@
     fun cond_tvars T =
       if internal then T
       else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
-    val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
+    val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
     val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
   in ((b, opt_T, mx), ctxt') end;
 
 in
 
 val read_var = prep_var Syntax.read_typ false;
-val cert_var = prep_var (K I) true;
+val cert_var = prep_var cert_typ true;
 
 end;