equal
deleted
inserted
replaced
60 let |
60 let |
61 val thy = ProofContext.theory_of ctxt |
61 val thy = ProofContext.theory_of ctxt |
62 val tyname = Sign.intern_type thy tystr |
62 val tyname = Sign.intern_type thy tystr |
63 val mapname = Sign.intern_const thy mapstr |
63 val mapname = Sign.intern_const thy mapstr |
64 val relname = Sign.intern_const thy relstr |
64 val relname = Sign.intern_const thy relstr |
|
65 |
|
66 fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt) |
|
67 handle _ => error ("Constant " ^ s ^ " not declared.") |
|
68 val _ = map check [mapname, relname] |
65 in |
69 in |
66 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
70 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
67 end |
71 end |
68 |
72 |
69 val maps_attr_parser = |
73 val maps_attr_parser = |