]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/hbugs/search_pattern_apply_tutor.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / hbugs / search_pattern_apply_tutor.ml
index 0c1e7d0ae24d547b61d48dce929cf3f7a1c6c0d7..1f5dad1bcdfe194f5a6e417c5ba437f2c2c743a2 100644 (file)
@@ -40,7 +40,7 @@ let slave mqi_handle (state, musing_id) =
       if uris = [] then
         Sorry
       else
-        Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris))
+        Eureka (Hints (List.map (fun uri -> Use_apply uri) uris))
     with Empty_must -> Sorry
   in
   let answer = Musing_completed (my_own_id, musing_id, hint) in