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.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.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.35 @@ -167,7 +167,7 @@
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.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.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.63  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
1.64    | prop_of (External (_, prop)) = prop;