equal
deleted
inserted
replaced
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 absF lthy (fastype_of rhs, lhs_ty) $ rhs |
44 val prop = Logic.mk_equals (lhs, absrep_trm) |
44 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy 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' |
47 |
47 |
48 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
48 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
49 |
49 |