changeset 42288 | 2074b31650e6 |
parent 40681 | 872b08416fb4 |
child 42361 | 23f352990944 |
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Fri Apr 08 14:20:57 2011 +0200 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Fri Apr 08 15:02:11 2011 +0200 @@ -51,7 +51,7 @@ fun mk_syntax name i = let - val syn = Syntax.escape name + val syn = Syntax_Ext.escape name val args = space_implode ",/ " (replicate i "_") in if i = 0 then Mixfix (syn, [], 1000)