equal
deleted
inserted
replaced
87 |
87 |
88 fun check_term' cnstr ctxt = |
88 fun check_term' cnstr ctxt = |
89 Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I) |
89 Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I) |
90 |
90 |
91 fun read_term' cnstr ctxt = |
91 fun read_term' cnstr ctxt = |
92 check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt |
92 check_term' cnstr ctxt o Syntax.parse_term ctxt |
93 |
93 |
94 val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term' |
94 val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term' |
95 val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term' |
95 val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term' |
96 |
96 |
97 |
97 |