equal
deleted
inserted
replaced
55 |
55 |
56 fun var_of T U = |
56 fun var_of T U = |
57 (case AList.lookup (op =) (!vars) (T, U) of |
57 (case AList.lookup (op =) (!vars) (T, U) of |
58 SOME V => V |
58 SOME V => V |
59 | NONE => |
59 | NONE => |
60 let val V = TVar ((Name.aT, length (!vars) + max_j), @{sort type}) in |
60 let val V = TVar ((Name.aT, length (!vars) + max_j), \<^sort>\<open>type\<close>) in |
61 vars := ((T, U), V) :: !vars; V |
61 vars := ((T, U), V) :: !vars; V |
62 end); |
62 end); |
63 |
63 |
64 fun gen (T as Type (s, Ts)) (U as Type (s', Us)) = |
64 fun gen (T as Type (s, Ts)) (U as Type (s', Us)) = |
65 if s = s' then Type (s, map2 gen Ts Us) else var_of T U |
65 if s = s' then Type (s, map2 gen Ts Us) else var_of T U |
104 |> Thm.close_derivation |
104 |> Thm.close_derivation |
105 end; |
105 end; |
106 |
106 |
107 val num_curry_uncurryN_balanced_precomp = 8; |
107 val num_curry_uncurryN_balanced_precomp = 8; |
108 val curry_uncurryN_balanced_precomp = |
108 val curry_uncurryN_balanced_precomp = |
109 map (mk_curry_uncurryN_balanced_raw @{context}) (0 upto num_curry_uncurryN_balanced_precomp); |
109 map (mk_curry_uncurryN_balanced_raw \<^context>) (0 upto num_curry_uncurryN_balanced_precomp); |
110 |
110 |
111 fun mk_curry_uncurryN_balanced ctxt n = |
111 fun mk_curry_uncurryN_balanced ctxt n = |
112 if n <= num_curry_uncurryN_balanced_precomp then nth curry_uncurryN_balanced_precomp n |
112 if n <= num_curry_uncurryN_balanced_precomp then nth curry_uncurryN_balanced_precomp n |
113 else mk_curry_uncurryN_balanced_raw ctxt n; |
113 else mk_curry_uncurryN_balanced_raw ctxt n; |
114 |
114 |