src/Pure/Tools/find_theorems.ML
changeset 43724 4e58485fa320
parent 43620 43a195a0279b
child 43731 70072780e095
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Jul 10 13:00:22 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Jul 10 13:51:21 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.make_list 
     1.8 -          (XML_Data.make_pair XML_Data.make_bool (single o xml_of_criterion)) criteria)
     1.9 +        XML.Elem (("Query", properties), XML_Data.Make.list
    1.10 +          (XML_Data.Make.pair XML_Data.Make.bool (single o xml_of_criterion)) criteria)
    1.11        end
    1.12    | xml_of_query _ = raise Fail "cannot serialize goal";
    1.13  
    1.14 @@ -148,8 +148,9 @@
    1.15        let
    1.16          val rem_dups = Properties.defined properties "rem_dups";
    1.17          val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
    1.18 -        val criteria = XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_bool 
    1.19 -          (criterion_of_xml o the_single)) body;
    1.20 +        val criteria =
    1.21 +          XML_Data.Dest.list (XML_Data.Dest.pair XML_Data.Dest.bool 
    1.22 +            (criterion_of_xml o the_single)) body;
    1.23        in
    1.24          {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
    1.25        end
    1.26 @@ -189,12 +190,12 @@
    1.27      val properties =
    1.28        if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
    1.29    in
    1.30 -    XML.Elem (("Result", properties), XML_Data.make_list (single o xml_of_theorem) theorems)
    1.31 +    XML.Elem (("Result", properties), XML_Data.Make.list (single o xml_of_theorem) theorems)
    1.32    end;
    1.33  
    1.34  fun result_of_xml (XML.Elem (("Result", properties), body)) =
    1.35        (Properties.get properties "found" |> Option.map Markup.parse_int,
    1.36 -       XML_Data.dest_list (theorem_of_xml o the_single) body)
    1.37 +       XML_Data.Dest.list (theorem_of_xml o the_single) body)
    1.38    | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
    1.39  
    1.40  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm