equal
deleted
inserted
replaced
61 val _ = sanity_test optbind lhs_str |
61 val _ = sanity_test optbind lhs_str |
62 |
62 |
63 val qconst_bname = Binding.name lhs_str |
63 val qconst_bname = Binding.name lhs_str |
64 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
64 val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
65 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
65 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
66 val (_, prop') = LocalDefs.cert_def lthy prop |
66 val (_, prop') = Local_Defs.cert_def lthy prop |
67 val (_, newrhs) = Primitive_Defs.abs_def prop' |
67 val (_, newrhs) = Primitive_Defs.abs_def prop' |
68 |
68 |
69 val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy |
69 val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy |
70 |
70 |
71 (* data storage *) |
71 (* data storage *) |