62 | [(binding, _, mx)] => |
62 | [(binding, _, mx)] => |
63 if Variable.check_name binding = lhs_str then (binding, mx) |
63 if Variable.check_name binding = lhs_str then (binding, mx) |
64 else error_msg binding lhs_str |
64 else error_msg binding lhs_str |
65 | _ => raise Match) |
65 | _ => raise Match) |
66 |
66 |
67 val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs |
67 val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs |
68 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
68 val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) |
69 val (_, prop') = Local_Defs.cert_def lthy prop |
69 val (_, prop') = Local_Defs.cert_def lthy prop |
70 val (_, newrhs) = Local_Defs.abs_def prop' |
70 val (_, newrhs) = Local_Defs.abs_def prop' |
71 |
71 |
72 val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy |
72 val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy |