src/Pure/Tools/find_theorems.ML
changeset 43767 e0219ef7f84c
parent 43731 70072780e095
child 46713 e6e1ec6d5c1c
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Jul 12 16:00:05 2011 +0900
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Jul 12 10:44:30 2011 +0200
     1.3 @@ -139,8 +139,8 @@
     1.4            |> (if rem_dups then cons ("rem_dups", "") else I)
     1.5            |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
     1.6        in
     1.7 -        XML.Elem (("Query", properties), XML_Data.Encode.list
     1.8 -          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
     1.9 +        XML.Elem (("Query", properties), XML.Encode.list
    1.10 +          (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
    1.11        end
    1.12    | xml_of_query _ = raise Fail "cannot serialize goal";
    1.13  
    1.14 @@ -149,7 +149,7 @@
    1.15          val rem_dups = Properties.defined properties "rem_dups";
    1.16          val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
    1.17          val criteria =
    1.18 -          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
    1.19 +          XML.Decode.list (XML.Decode.pair XML.Decode.bool
    1.20              (criterion_of_xml o the_single)) body;
    1.21        in
    1.22          {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
    1.23 @@ -190,12 +190,12 @@
    1.24      val properties =
    1.25        if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
    1.26    in
    1.27 -    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
    1.28 +    XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
    1.29    end;
    1.30  
    1.31  fun result_of_xml (XML.Elem (("Result", properties), body)) =
    1.32        (Properties.get properties "found" |> Option.map Markup.parse_int,
    1.33 -       XML_Data.Decode.list (theorem_of_xml o the_single) body)
    1.34 +       XML.Decode.list (theorem_of_xml o the_single) body)
    1.35    | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
    1.36  
    1.37  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm