prep_mixfix': proper use of Syntax.literal;
authorwenzelm
Wed, 30 Jan 2002 14:00:25 +0100
changeset 12863 cc4dd256564f
parent 12862 c66cb5591191
child 12864 cecaa6e64fd5
prep_mixfix': proper use of Syntax.literal;
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;