equal
deleted
inserted
replaced
278 | SOME {tcs, ...} => tcs); |
278 | SOME {tcs, ...} => tcs); |
279 val i = getOpt (opt_i, 1); |
279 val i = getOpt (opt_i, 1); |
280 val tc = List.nth (tcs, i - 1) handle Subscript => |
280 val tc = List.nth (tcs, i - 1) handle Subscript => |
281 error ("No termination condition #" ^ string_of_int i ^ |
281 error ("No termination condition #" ^ string_of_int i ^ |
282 " in recdef definition of " ^ quote name); |
282 " in recdef definition of " ^ quote name); |
283 in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end; |
283 in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end; |
284 |
284 |
285 val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const; |
285 val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const; |
286 val recdef_tc_i = gen_recdef_tc (K I) (K I); |
286 val recdef_tc_i = gen_recdef_tc (K I) (K I); |
287 |
287 |
288 |
288 |