equal
deleted
inserted
replaced
51 let |
51 let |
52 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
52 val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." |
53 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
53 val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" |
54 |
54 |
55 val qconst_bname = Binding.name lhs_str |
55 val qconst_bname = Binding.name lhs_str |
56 val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
56 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
57 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
57 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
58 val (_, prop') = LocalDefs.cert_def lthy prop |
58 val (_, prop') = LocalDefs.cert_def lthy prop |
59 val (_, newrhs) = Primitive_Defs.abs_def prop' |
59 val (_, newrhs) = Primitive_Defs.abs_def prop' |
60 |
60 |
61 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |
61 val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy |