# HG changeset patch
# User wenzelm
# Date 1152651639 -7200
# Node ID a8d73903dc720d9bc0fd8e5fe23f13cf98132d3a
# Parent  c96cb48eef530f93f9e5fecc3c23d1e20c68fa2c
adapted Name.defaults_of;

diff -r c96cb48eef53 -r a8d73903dc72 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 11 23:00:37 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 11 23:00:39 2006 +0200
@@ -1247,7 +1247,7 @@
     val prt_defT = prt_atom prt_var prt_typ;
     val prt_defS = prt_atom prt_varT prt_sort;
 
-    val (types, sorts, used, _, _) = Variable.defaults_of ctxt;
+    val (types, sorts, used, _) = Variable.defaults_of ctxt;
   in
     verb single (K pretty_thy) @
     pretty_ctxt ctxt @