src/Tools/Compute_Oracle/compute.ML
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