equal
deleted
inserted
replaced
43 |
43 |
44 |
44 |
45 (* Check for all sorts of errors in the input - nominal needs a different checking function *) |
45 (* Check for all sorts of errors in the input - nominal needs a different checking function *) |
46 fun nominal_check_defs ctxt fixes eqs = |
46 fun nominal_check_defs ctxt fixes eqs = |
47 let |
47 let |
48 val _ = tracing ("fixes: " ^ @{make_string} fixes) |
|
49 |
|
50 val fnames = map (fst o fst) fixes |
48 val fnames = map (fst o fst) fixes |
51 |
49 |
52 fun check geq = |
50 fun check geq = |
53 let |
51 let |
54 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
52 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |