equal
deleted
inserted
replaced
66 fun thy_arity (dbind, tvars, mx) = |
66 fun thy_arity (dbind, tvars, mx) = |
67 ((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false) |
67 ((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false) |
68 |
68 |
69 (* this theory is used just for parsing and error checking *) |
69 (* this theory is used just for parsing and error checking *) |
70 val tmp_thy = thy |
70 val tmp_thy = thy |
71 |> Theory.copy |
|
72 |> fold (add_arity o thy_arity) dtnvs |
71 |> fold (add_arity o thy_arity) dtnvs |
73 |
72 |
74 val dbinds : binding list = |
73 val dbinds : binding list = |
75 map (fn (_,dbind,_,_) => dbind) raw_specs |
74 map (fn (_,dbind,_,_) => dbind) raw_specs |
76 val raw_rhss : |
75 val raw_rhss : |