X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ffilter_auto.ml;fp=helm%2Focaml%2Ftactics%2Ffilter_auto.ml;h=73eaed638c4aee767a317f4431c3bf246fefa774;hb=16d6d961a5d7db08bfdf1bccae7f36c6b2fd7fe2;hp=6fae7b7377aa0c1f88794e19a75eb6b3c477be56;hpb=3fd8583f198e7e09995c3a65b5f05a853c8d1646;p=helm.git

diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml
index 6fae7b737..73eaed638 100644
--- a/helm/ocaml/tactics/filter_auto.ml
+++ b/helm/ocaml/tactics/filter_auto.ml
@@ -32,8 +32,10 @@ let main_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConc
 
 let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;;
 
+let escape = Str.global_replace (Str.regexp_string "\'") "\\'";;
 
 let hyp_const (conn:Mysql.dbd) uri =
+  let uri = escape uri in
   (*query to obtain all the constants in the hypothesis of the theorem*)
   let query =
      "select h_occurrence from refObj where source='"^uri^