Syntax.internal thesis;

--- 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);