]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/metadata/create2/touch/touch.ml
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / metadata / create2 / touch / touch.ml
index 8538a8faa7750033aeb21126b9c79e12d96828bc..8fea03e0e90b85e7ce03b6a455d421c870483e0d 100644 (file)
@@ -60,12 +60,7 @@ let touch_file rdf_string_uri =
 
 let get_obj uri =
  let cicfilename = Getter.getxml uri in
-  let res =
-   match CicParser.term_of_xml cicfilename uri false with
-      (annobj, None) ->
-        Deannotate.deannotate_obj annobj
-    | _ -> assert false
-  in
+  let res = CicParser.obj_of_xml cicfilename uri in
    Unix.unlink cicfilename ;
    res
 ;;