src/Pure/Syntax/syntax_phases.ML
changeset 53297 7746c9f1baf3
parent 53280 36ffe23b25f8
child 53299 896ebb4646d8
     1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun May 26 20:08:53 2013 +0200
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun May 26 20:42:43 2013 +0200
     1.3 @@ -517,7 +517,7 @@
     1.4      val {structs, fixes} = idents;
     1.5  
     1.6      fun mark_atoms ((t as Const (c, _)) $ u) =
     1.7 -          if member (op =) Syntax.token_markers c
     1.8 +          if member (op =) Pure_Thy.token_markers c
     1.9            then t $ u else mark_atoms t $ mark_atoms u
    1.10        | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
    1.11        | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)