equal
deleted
inserted
replaced
63 val thy = ProofContext.theory_of ctxt |
63 val thy = ProofContext.theory_of ctxt |
64 val tyname = Sign.intern_type thy tystr |
64 val tyname = Sign.intern_type thy tystr |
65 val mapname = Sign.intern_const thy mapstr |
65 val mapname = Sign.intern_const thy mapstr |
66 val relname = Sign.intern_const thy relstr |
66 val relname = Sign.intern_const thy relstr |
67 |
67 |
68 (* FIXME: if you don't handle the error you also get an error with a similar message: No such constant: "bla" *) |
68 fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt) |
69 fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt) |
69 val _ = map sanity_check [mapname, relname] |
70 handle _ => error ("Constant " ^ s ^ " not declared.") |
|
71 val _ = map check [mapname, relname] |
|
72 in |
70 in |
73 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
71 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
74 end |
72 end |
75 |
73 |
76 val maps_attr_parser = |
74 val maps_attr_parser = |