99 val cT = extraTs ---> Ts ---> T |
99 val cT = extraTs ---> Ts ---> T |
100 val c = Const (Sign.full_name thy cname, cT) |
100 val c = Const (Sign.full_name thy cname, cT) |
101 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
101 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
102 (*Forms a lambda-abstraction over the formal parameters*) |
102 (*Forms a lambda-abstraction over the formal parameters*) |
103 val _ = Output.debug (fn () => "declaring the constant " ^ cname) |
103 val _ = Output.debug (fn () => "declaring the constant " ^ cname) |
104 val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy |
104 val thy' = |
|
105 Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy |
105 (*Theory is augmented with the constant, then its def*) |
106 (*Theory is augmented with the constant, then its def*) |
106 val cdef = cname ^ "_def" |
107 val cdef = cname ^ "_def" |
107 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' |
108 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' |
108 handle ERROR _ => raise Clausify_failure thy' |
109 handle ERROR _ => raise Clausify_failure thy' |
109 in dec_sko (subst_bound (list_comb(c,args), p)) |
110 in dec_sko (subst_bound (list_comb(c,args), p)) |
271 | [] => |
272 | [] => |
272 let val _ = Output.debug (fn()=>"Lookup was empty"); |
273 let val _ = Output.debug (fn()=>"Lookup was empty"); |
273 val Ts = map type_of args |
274 val Ts = map type_of args |
274 val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu')) |
275 val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu')) |
275 val c = Const (Sign.full_name thy cname, cT) |
276 val c = Const (Sign.full_name thy cname, cT) |
276 val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy |
277 val thy = |
|
278 Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy |
277 (*Theory is augmented with the constant, |
279 (*Theory is augmented with the constant, |
278 then its definition*) |
280 then its definition*) |
279 val cdef = cname ^ "_def" |
281 val cdef = cname ^ "_def" |
280 val thy = Theory.add_defs_i false false |
282 val thy = Theory.add_defs_i false false |
281 [(cdef, equals cT $ c $ rhs)] thy |
283 [(cdef, equals cT $ c $ rhs)] thy |