equal
deleted
inserted
replaced
17 (* actual code *) |
17 (* actual code *) |
18 |
18 |
19 fun close_form t = |
19 fun close_form t = |
20 fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t)) |
20 fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t)) |
21 (map dest_Free (Misc_Legacy.term_frees t)) t |
21 (map dest_Free (Misc_Legacy.term_frees t)) t |
|
22 |
|
23 fun add_final overloaded (c, T) thy = |
|
24 let |
|
25 val ctxt = Syntax.init_pretty_global thy; |
|
26 val _ = Theory.check_overloading ctxt overloaded (c, T); |
|
27 in Theory.add_deps ctxt "" (c, T) [] thy end; |
22 |
28 |
23 local |
29 local |
24 fun mk_definitional [] arg = arg |
30 fun mk_definitional [] arg = arg |
25 | mk_definitional ((thname,cname,covld)::cos) (thy,thm) = |
31 | mk_definitional ((thname,cname,covld)::cos) (thy,thm) = |
26 case HOLogic.dest_Trueprop (concl_of thm) of |
32 case HOLogic.dest_Trueprop (concl_of thm) of |
56 val ctype = domain_type (type_of P) |
62 val ctype = domain_type (type_of P) |
57 val cname_full = Sign.intern_const thy cname |
63 val cname_full = Sign.intern_const thy cname |
58 val cdefname = if thname = "" |
64 val cdefname = if thname = "" |
59 then Thm.def_name (Long_Name.base_name cname) |
65 then Thm.def_name (Long_Name.base_name cname) |
60 else thname |
66 else thname |
61 val co = Const(cname_full,ctype) |
67 val thy' = add_final covld (cname_full,ctype) thy |
62 val thy' = Theory.add_finals_i covld [co] thy |
68 val co = Const (cname_full,ctype) |
63 val tm' = case P of |
69 val tm' = case P of |
64 Abs(_, _, bodt) => subst_bound (co, bodt) |
70 Abs(_, _, bodt) => subst_bound (co, bodt) |
65 | _ => P $ co |
71 | _ => P $ co |
66 in |
72 in |
67 process cos (thy',tm') |
73 process cos (thy',tm') |