51 |
51 |
52 val concl = #2 o R.dest_thm; |
52 val concl = #2 o R.dest_thm; |
53 val hyp = #1 o R.dest_thm; |
53 val hyp = #1 o R.dest_thm; |
54 |
54 |
55 val list_mk_type = U.end_itlist (curry (op -->)); |
55 val list_mk_type = U.end_itlist (curry (op -->)); |
56 |
|
57 fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1)); |
|
58 |
56 |
59 fun front_last [] = raise TFL_ERR "front_last" "empty list" |
57 fun front_last [] = raise TFL_ERR "front_last" "empty list" |
60 | front_last [x] = ([],x) |
58 | front_last [x] = ([],x) |
61 | front_last (h::t) = |
59 | front_last (h::t) = |
62 let val (pref,x) = front_last t |
60 let val (pref,x) = front_last t |
326 val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L) |
324 val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L) |
327 val atom = single (distinct (op aconv) funcs) |
325 val atom = single (distinct (op aconv) funcs) |
328 val (fname,ftype) = dest_atom atom |
326 val (fname,ftype) = dest_atom atom |
329 val dummy = map (no_repeat_vars thy) pats |
327 val dummy = map (no_repeat_vars thy) pats |
330 val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats, |
328 val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats, |
331 map (fn (t,i) => (t,(i,true))) (enumerate R)) |
329 map_index (fn (i, t) => (t,(i,true))) R) |
332 val names = List.foldr OldTerm.add_term_names [] R |
330 val names = List.foldr OldTerm.add_term_names [] R |
333 val atype = type_of(hd pats) |
331 val atype = type_of(hd pats) |
334 and aname = Name.variant names "a" |
332 and aname = Name.variant names "a" |
335 val a = Free(aname,atype) |
333 val a = Free(aname,atype) |
336 val ty_info = Thry.match_info thy |
334 val ty_info = Thry.match_info thy |