Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adapted PThm and MinProof;
authorwenzelm
Sat, 15 Nov 2008 21:31:37 +0100
changeset 28811 aa36d05926ec
parent 28810 e915ab11fe52
child 28812 413695e07bd4
adapted PThm and MinProof;
src/HOL/Import/xmlconv.ML file | annotate | diff | comparison | revisions
src/Pure/Tools/xml_syntax.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/xmlconv.ML	Sat Nov 15 21:31:36 2008 +0100
+++ b/src/HOL/Import/xmlconv.ML	Sat Nov 15 21:31:37 2008 +0100
@@ -143,13 +143,13 @@
   | xml_of_proof (prf %% prf') =
       XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
   | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
-  | xml_of_proof (PThm (s, _, t, optTs)) =
+  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
       XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
   | xml_of_proof (PAxm (s, t, optTs)) =
       XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
   | xml_of_proof (Oracle (s, t, optTs)) =
       XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
-  | xml_of_proof (MinProof _) = XML.Elem ("MinProof", [], []);
+  | xml_of_proof MinProof = XML.Elem ("MinProof", [], []);
 
 fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
 fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])
--- a/src/Pure/Tools/xml_syntax.ML	Sat Nov 15 21:31:36 2008 +0100
+++ b/src/Pure/Tools/xml_syntax.ML	Sat Nov 15 21:31:37 2008 +0100
@@ -71,13 +71,13 @@
   | xml_of_proof (prf %% prf') =
       XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
   | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
-  | xml_of_proof (PThm (s, _, t, optTs)) =
+  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
       XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
   | xml_of_proof (PAxm (s, t, optTs)) =
       XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
   | xml_of_proof (Oracle (s, t, optTs)) =
       XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
-  | xml_of_proof (MinProof prfs) =
+  | xml_of_proof MinProof =
       XML.Elem ("MinProof", [], []);
 
 (* useful for checking the output against a schema file *)
@@ -157,13 +157,14 @@
   | proof_of_xml (XML.Elem ("Hyp", [], [term])) =
       Hyp (term_of_xml term)
   | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
-      PThm (s, MinProof ([], [], []),  (* FIXME? *)
-        term_of_xml term, opttypes_of_xml opttypes)
+      (* FIXME? *)
+      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
+        Lazy.value (Proofterm.make_proof_body MinProof)))
   | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
       PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
       Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
-  | proof_of_xml (XML.Elem ("MinProof", _, _)) = MinProof ([], [], [])
+  | proof_of_xml (XML.Elem ("MinProof", _, _)) = MinProof
   | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
 
 end;
isabelle