# HG changeset patch
# User wenzelm
# Date 1012395625 -3600
# Node ID cc4dd256564fa01eb0f29d4a76a1347381b89aee
# Parent  c66cb5591191146a9ac79a32f41836436992fbcc
prep_mixfix': proper use of Syntax.literal;

diff -r c66cb5591191 -r cc4dd256564f src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jan 30 13:59:57 2002 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Jan 30 14:00:25 2002 +0100
@@ -351,7 +351,7 @@
 
 fun prep_mixfix' (_, _, None) = None
   | prep_mixfix' (x, _, Some Syntax.NoSyn) = None
-  | prep_mixfix' (x, opt_T, _) = Some (x, mixfix x opt_T (Syntax.Delimfix x));
+  | prep_mixfix' (x, opt_T, _) = Some (x, mixfix x opt_T (Syntax.literal x));
 
 fun prep_struct (x, _, None) = Some x
   | prep_struct _ = None;