legacy_intern_skolem: legacy_feature;

--- a/src/Pure/Isar/proof_context.ML	Tue May 08 15:01:31 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue May 08 15:01:33 2007 +0200
@@ -486,7 +486,7 @@
     val is_declared = is_some (def_type (x, ~1));
     val res =
       if is_free andalso not is_internal then (no_skolem false x; sko)
-      else ((no_skolem false x; ()) handle ERROR msg => warning msg;
+      else ((no_skolem false x; ()) handle ERROR msg => legacy_feature msg;
         if is_internal andalso is_declared then SOME x else NONE);
   in if is_some res then res else if is_declared then SOME x else NONE end;