diff -r f42de6d8ed8e -r b7add947a6ef src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 13 15:05:56 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 13 17:26:22 2014 +0100
@@ -219,9 +219,12 @@
 (
   type T = data;
   fun init thy =
-    make_data (mode_default, Local_Syntax.init thy,
-      (Sign.tsig_of thy, Sign.tsig_of thy),
-      (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases);
+    make_data (mode_default,
+      Local_Syntax.init thy,
+      (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
+      (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
+      Facts.empty,
+      empty_cases);
 );
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);