src/Pure/Tools/find_theorems.ML
changeset 50217 ce1f0602f48e
parent 50214 67fb9a168d10
child 51658 21c10672633b
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Nov 26 16:22:29 2012 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 26 16:28:22 2012 +0100
     1.3 @@ -116,17 +116,17 @@
     1.4    | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
     1.5    | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
     1.6    | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
     1.7 -  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat])
     1.8 -  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]);
     1.9 +  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat])
    1.10 +  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]);
    1.11  
    1.12  fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
    1.13    | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
    1.14    | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
    1.15    | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
    1.16    | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
    1.17 -  | criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree)
    1.18 -  | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
    1.19 -  | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
    1.20 +  | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree)
    1.21 +  | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree)
    1.22 +  | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
    1.23  
    1.24  fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
    1.25        let
    1.26 @@ -149,7 +149,7 @@
    1.27        in
    1.28          {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
    1.29        end
    1.30 -  | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
    1.31 +  | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree);
    1.32  
    1.33  
    1.34  
    1.35 @@ -167,7 +167,7 @@
    1.36  
    1.37  fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
    1.38    | xml_of_theorem (External (fact_ref, prop)) =
    1.39 -      XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
    1.40 +      XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]);
    1.41  
    1.42  fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
    1.43        let
    1.44 @@ -177,9 +177,9 @@
    1.45            Option.map (single o Facts.Single o Markup.parse_int)
    1.46              (Properties.get properties "index");
    1.47        in
    1.48 -        External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
    1.49 +        External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree)
    1.50        end
    1.51 -  | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
    1.52 +  | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
    1.53  
    1.54  fun xml_of_result (opt_found, theorems) =
    1.55    let
    1.56 @@ -192,7 +192,7 @@
    1.57  fun result_of_xml (XML.Elem (("Result", properties), body)) =
    1.58        (Properties.get properties "found" |> Option.map Markup.parse_int,
    1.59         XML.Decode.list (theorem_of_xml o the_single) body)
    1.60 -  | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
    1.61 +  | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree);
    1.62  
    1.63  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
    1.64    | prop_of (External (_, prop)) = prop;