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 check s = (Const (s, dummyT) |> Syntax.check_term ctxt) |
69 fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt) |
69 handle _ => error ("Constant " ^ s ^ " not declared.") |
70 handle _ => error ("Constant " ^ s ^ " not declared.") |
70 val _ = map check [mapname, relname] |
71 val _ = map check [mapname, relname] |
71 in |
72 in |
72 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |
73 maps_attribute_aux tyname {mapfun = mapname, relfun = relname} |