# HG changeset patch
# User wenzelm
# Date 1120050816 -7200
# Node ID e45c9a95a554e8b50f0d1c5f780bb2669a449559
# Parent  4590c1f790508204174cf584907a0032f15c4281
no Syntax.internal on thesis;

diff -r 4590c1f79050 -r e45c9a95a554 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jun 29 15:13:35 2005 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jun 29 15:13:36 2005 +0200
@@ -83,7 +83,7 @@
     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
 
     (*obtain statements*)
-    val thesisN = Term.variant xs (Syntax.internal AutoBind.thesisN);
+    val thesisN = Term.variant xs AutoBind.thesisN;
     val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN];
     val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment sign thesisN);
     val bound_thesis_raw as (bound_thesis_name, _) =