# HG changeset patch
# User wenzelm
# Date 1028625647 -7200
# Node ID f93f7d76689542be54566f2a5b3e2a026709ea84
# Parent  ced7a699282b5f0d45acde19289917050e07a97a
fixed intern_skolem: disallow internal names (why didn't anybody notice?!?);

diff -r ced7a699282b -r f93f7d766895 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Aug 06 11:19:52 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Aug 06 11:20:47 2002 +0200
@@ -28,7 +28,6 @@
   val cert_typ: context -> typ -> typ
   val cert_typ_no_norm: context -> typ -> typ
   val get_skolem: context -> string -> string
-  val intern_skolem: context -> term -> term
   val extern_skolem: context -> term -> term
   val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
   val read_term: context -> string -> term
@@ -444,7 +443,7 @@
 fun intern_skolem ctxt =
   let
     fun intern (t as Free (x, T)) =
-          (case lookup_skolem ctxt (no_skolem true ctxt x) of
+          (case lookup_skolem ctxt (no_skolem false ctxt x) of
             Some x' => Free (x', T)
           | None => t)
       | intern (t $ u) = intern t $ intern u