equal
deleted
inserted
replaced
36 (* returns the defined constant and its definition *) |
36 (* returns the defined constant and its definition *) |
37 (* theorem; stores the data in the qconsts slot *) |
37 (* theorem; stores the data in the qconsts slot *) |
38 |
38 |
39 fun quotient_def mx attr lhs rhs lthy = |
39 fun quotient_def mx attr lhs rhs lthy = |
40 let |
40 let |
41 val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.) |
41 val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*) |
42 val qconst_bname = Binding.name lhs_str; |
42 val qconst_bname = Binding.name lhs_str; |
43 val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs |
43 val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs |
44 val prop = Logic.mk_equals (lhs, absrep_trm) |
44 val prop = Logic.mk_equals (lhs, absrep_trm) |
45 val (_, prop') = LocalDefs.cert_def lthy prop |
45 val (_, prop') = LocalDefs.cert_def lthy prop |
46 val (_, newrhs) = Primitive_Defs.abs_def prop' |
46 val (_, newrhs) = Primitive_Defs.abs_def prop' |