equal
deleted
inserted
replaced
89 |
89 |
90 fun gen_add_judgment add_consts (b, T, mx) thy = |
90 fun gen_add_judgment add_consts (b, T, mx) thy = |
91 let |
91 let |
92 val c = Sign.full_name thy b; |
92 val c = Sign.full_name thy b; |
93 val thy' = thy |> add_consts [(b, T, mx)]; |
93 val thy' = thy |> add_consts [(b, T, mx)]; |
94 val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c); |
|
95 in |
94 in |
96 thy' |
95 thy' |
97 |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) [] |
96 |> Theory.add_deps_const c |
98 |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) => |
97 |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) => |
99 if is_some judgment then error "Attempt to redeclare object-logic judgment" |
98 if is_some judgment then error "Attempt to redeclare object-logic judgment" |
100 else (base_sort, SOME c, atomize_rulify)) |
99 else (base_sort, SOME c, atomize_rulify)) |
101 end; |
100 end; |
102 |
101 |