# HG changeset patch
# User wenzelm
# Date 1007595783 -3600
# Node ID 968213967c07cccc4a398aa8a01d8758df7263b6
# Parent  3e3bd3d449b5c32c5c7d6c6aa5d1ed4f6ffb6a30
Syntax.internal thesis;

diff -r 3e3bd3d449b5 -r 968213967c07 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Dec 06 00:42:24 2001 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Dec 06 00:43:03 2001 +0100
@@ -82,7 +82,7 @@
     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
 
     (*that_prop*)
-    val thesisN = Term.variant xs AutoBind.thesisN;
+    val thesisN = Term.variant xs (Syntax.internal AutoBind.thesisN);
     val bound_thesis =
       ProofContext.bind_skolem fix_ctxt [thesisN] (ObjectLogic.fixed_judgment sign thesisN);