changeset 24137 | 8d7896398147 |
parent 23663 | 84b5c89b8b49 |
child 24584 | 01e83ffa6c54 |
--- a/src/Tools/Compute_Oracle/compute.ML Thu Aug 02 23:18:13 2007 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Fri Aug 03 16:28:15 2007 +0200 @@ -267,7 +267,7 @@ val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable - in Computer (Theory.self_ref thy, encoding, Termtab.keys hyptable, shyptable, prog) end + in Computer (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog) end (*fun timeit f = let