equal
deleted
inserted
replaced
336 $ functional |
336 $ functional |
337 val (_, def_term, _) = |
337 val (_, def_term, _) = |
338 Sign.infer_types (sign_of thy) (K None) (K None) [] false |
338 Sign.infer_types (sign_of thy) (K None) (K None) [] false |
339 ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], |
339 ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], |
340 propT) |
340 propT) |
341 in Theory.add_defs_i [(def_name, def_term)] thy end |
341 in PureThy.add_store_defs_i [(def_name, def_term)] thy end |
342 end; |
342 end; |
343 |
343 |
344 |
344 |
345 |
345 |
346 (*--------------------------------------------------------------------------- |
346 (*--------------------------------------------------------------------------- |
456 val (extractants,TCl) = ListPair.unzip extracta |
456 val (extractants,TCl) = ListPair.unzip extracta |
457 val TCs = foldr (gen_union (op aconv)) (TCl, []) |
457 val TCs = foldr (gen_union (op aconv)) (TCl, []) |
458 val full_rqt = WFR::TCs |
458 val full_rqt = WFR::TCs |
459 val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt} |
459 val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt} |
460 val R'abs = S.rand R' |
460 val R'abs = S.rand R' |
461 val theory = Theory.add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)] |
461 val theory = PureThy.add_store_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)] |
462 thy |
462 thy |
463 val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq) |
463 val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq) |
464 val fconst = #lhs(S.dest_eq(concl def)) |
464 val fconst = #lhs(S.dest_eq(concl def)) |
465 val tych = Thry.typecheck theory |
465 val tych = Thry.typecheck theory |
466 val baz = R.DISCH (tych proto_def) |
466 val baz = R.DISCH (tych proto_def) |