Syntax.internal thesis;
authorwenzelm
Thu Dec 06 00:43:03 2001 +0100 (2001-12-06)
changeset 12404968213967c07
parent 12403 3e3bd3d449b5
child 12405 9b16f99fd7b9
Syntax.internal thesis;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Dec 06 00:42:24 2001 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Dec 06 00:43:03 2001 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
     1.5  
     1.6      (*that_prop*)
     1.7 -    val thesisN = Term.variant xs AutoBind.thesisN;
     1.8 +    val thesisN = Term.variant xs (Syntax.internal AutoBind.thesisN);
     1.9      val bound_thesis =
    1.10        ProofContext.bind_skolem fix_ctxt [thesisN] (ObjectLogic.fixed_judgment sign thesisN);
    1.11