equal
deleted
inserted
replaced
92 |
92 |
93 structure Datatype = |
93 structure Datatype = |
94 struct |
94 struct |
95 local |
95 local |
96 |
96 |
97 val mysort = sort; |
|
98 open ThyParse HOLogic; |
97 open ThyParse HOLogic; |
99 exception Impossible; |
98 exception Impossible; |
100 exception RecError of string; |
99 exception RecError of string; |
101 |
100 |
102 val is_dtRek = (fn dtRek _ => true | _ => false); |
101 val is_dtRek = (fn dtRek _ => true | _ => false); |
173 |
172 |
174 (* check function specified for all constructors and sort function terms *) |
173 (* check function specified for all constructors and sort function terms *) |
175 |
174 |
176 fun check_and_sort (n,its) = |
175 fun check_and_sort (n,its) = |
177 if length its = n |
176 if length its = n |
178 then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its) |
177 then map snd (Library.sort (make_ord (fn ((i : int,_),(j,_)) => i<j)) its) |
179 else raise error "Primrec definition error:\n\ |
178 else raise error "Primrec definition error:\n\ |
180 \Please give an equation for every constructor"; |
179 \Please give an equation for every constructor"; |
181 |
180 |
182 (* translate rec equations into function arguments suitable for rec comb *) |
181 (* translate rec equations into function arguments suitable for rec comb *) |
183 (* theory parameter needed for printing error messages *) |
182 (* theory parameter needed for printing error messages *) |