equal
deleted
inserted
replaced
1324 | (_, qs, _) => qs) |
1324 | (_, qs, _) => qs) |
1325 in |
1325 in |
1326 thy |
1326 thy |
1327 |> Sign.root_path |
1327 |> Sign.root_path |
1328 |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers |
1328 |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers |
1329 |> f bnf |
1329 |> (fn thy => f (morph_bnf (Morphism.transfer_morphism thy) bnf) thy) |
1330 |> Sign.restore_naming thy |
1330 |> Sign.restore_naming thy |
1331 end; |
1331 end; |
1332 |
1332 |
1333 val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path; |
1333 val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path; |
1334 |
1334 |
1420 (Scan.option ((Parse.reserved "wits" -- @{keyword ":"}) |-- |
1420 (Scan.option ((Parse.reserved "wits" -- @{keyword ":"}) |-- |
1421 Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) >> the_default []) -- |
1421 Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) >> the_default []) -- |
1422 Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) |
1422 Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) |
1423 >> bnf_cmd); |
1423 >> bnf_cmd); |
1424 |
1424 |
|
1425 val _ = Context.>> (Context.map_theory BNF_Interpretation.init); |
|
1426 |
1425 end; |
1427 end; |