# HG changeset patch
# User wenzelm
# Date 1178629293 -7200
# Node ID 165f733c50bd9fb47e1a1fe6069e591801a7d4bd
# Parent  9de680b7d8194a79408abc261c81e2f097075898
legacy_intern_skolem: legacy_feature;

diff -r 9de680b7d819 -r 165f733c50bd src/Pure/Isar/proof_context.ML
--- 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;