87 | term_ord' pr thy (t, u) = |
87 | term_ord' pr thy (t, u) = |
88 (if pr then |
88 (if pr then |
89 let |
89 let |
90 val (f, ts) = strip_comb t and (g, us) = strip_comb u; |
90 val (f, ts) = strip_comb t and (g, us) = strip_comb u; |
91 val _=writeln("t= f@ts= \""^ |
91 val _=writeln("t= f@ts= \""^ |
92 ((string_of_cterm o (Thm.cterm thy)) f)^"\" @ \"["^ |
92 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ |
93 (commas(map(string_of_cterm o (Thm.cterm thy)) ts))^"]\""); |
93 (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\""); |
94 val _=writeln("u= g@us= \""^ |
94 val _=writeln("u= g@us= \""^ |
95 ((string_of_cterm o (Thm.cterm thy)) g)^"\" @ \"["^ |
95 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ |
96 (commas(map(string_of_cterm o (Thm.cterm thy)) us))^"]\""); |
96 (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\""); |
97 val _=writeln("size_of_term(t,u)= ("^ |
97 val _=writeln("size_of_term(t,u)= ("^ |
98 (string_of_int(size_of_term' t))^", "^ |
98 (string_of_int(size_of_term' t))^", "^ |
99 (string_of_int(size_of_term' u))^")"); |
99 (string_of_int(size_of_term' u))^")"); |
100 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g))); |
100 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g))); |
101 val _=writeln("terms_ord(ts,us) = "^ |
101 val _=writeln("terms_ord(ts,us) = "^ |