equal
deleted
inserted
replaced
34 |
34 |
35 fun quotient_def mx attr lhs rhs lthy = |
35 fun quotient_def mx attr lhs rhs lthy = |
36 let |
36 let |
37 val Free (lhs_str, lhs_ty) = lhs; |
37 val Free (lhs_str, lhs_ty) = lhs; |
38 val qconst_bname = Binding.name lhs_str; |
38 val qconst_bname = Binding.name lhs_str; |
39 val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
39 val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs |
40 |> Syntax.check_term lthy |
|
41 val prop = Logic.mk_equals (lhs, absrep_trm) |
40 val prop = Logic.mk_equals (lhs, absrep_trm) |
42 val (_, prop') = LocalDefs.cert_def lthy prop |
41 val (_, prop') = LocalDefs.cert_def lthy prop |
43 val (_, newrhs) = Primitive_Defs.abs_def prop' |
42 val (_, newrhs) = Primitive_Defs.abs_def prop' |
44 |
43 |
45 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
44 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |