src/Pure/Tools/find_theorems.ML

--- a/src/Pure/Tools/find_theorems.ML	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/Tools/find_theorems.ML	Tue Jul 12 10:44:30 2011 +0200
@@ -139,8 +139,8 @@
           |> (if rem_dups then cons ("rem_dups", "") else I)
           |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
       in
-        XML.Elem (("Query", properties), XML_Data.Encode.list
-          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
+        XML.Elem (("Query", properties), XML.Encode.list
+          (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
       end
   | xml_of_query _ = raise Fail "cannot serialize goal";
 
@@ -149,7 +149,7 @@
         val rem_dups = Properties.defined properties "rem_dups";
         val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
         val criteria =
-          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
+          XML.Decode.list (XML.Decode.pair XML.Decode.bool
             (criterion_of_xml o the_single)) body;
       in
         {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
@@ -190,12 +190,12 @@
     val properties =
       if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   in
-    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
+    XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
   end;
 
 fun result_of_xml (XML.Elem (("Result", properties), body)) =
       (Properties.get properties "found" |> Option.map Markup.parse_int,
-       XML_Data.Decode.list (theorem_of_xml o the_single) body)
+       XML.Decode.list (theorem_of_xml o the_single) body)
   | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
 
 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm