equal
deleted
inserted
replaced
237 (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy |
237 (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy |
238 end |
238 end |
239 |
239 |
240 (* outer syntax *) |
240 (* outer syntax *) |
241 |
241 |
242 local structure P = OuterParse and K = OuterSyntax.Keyword in |
242 local structure P = OuterParse and K = OuterKeyword in |
243 |
243 |
244 (* taken from ~~/Pure/Isar/isar_syn.ML *) |
244 (* taken from ~~/Pure/Isar/isar_syn.ML *) |
245 val opt_overloaded = |
245 val opt_overloaded = |
246 Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false |
246 Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false |
247 |
247 |