Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/datatype_rep_proofs.ML
changeset 21291 d59cbb8ce002
parent 21021 6f19e5eb3a44
child 21365 4ee8e2702241 
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Nov 10 20:58:48 2006 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Nov 10 22:18:51 2006 +0100
@@ -179,7 +179,7 @@
          InductivePackage.add_inductive_i false big_rec_name false true false
            (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
            (map (fn x => (("", []), x)) intr_ts) [] #>
-         apfst (snd o LocalTheory.exit false)) thy1;
+         apfst (ProofContext.theory_of o LocalTheory.exit)) thy1;
 
     (********************************* typedef ********************************)
isabelle