src/HOL/Tools/BNF/bnf_def.ML
changeset 56522 f54003750e7d
parent 56376 5a93b8f928a2
child 56523 2ae16e3d8b6d
equal deleted inserted replaced
56521:20cfb18a53ba 56522:f54003750e7d
  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;