# HG changeset patch
# User wenzelm
# Date 1434286779 -7200
# Node ID 4ba2a8bc5c362fad64c34397e61658039a3e1469
# Parent  7bd794d7c86b51c9aed6a2e23e2ed1316724ebe0
tuned;

diff -r 7bd794d7c86b -r 4ba2a8bc5c36 src/Pure/Isar/proof_context.ML
--- 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;