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/HOLCF/Tools/Domain/domain_isomorphism.ML
changeset 58936 7fbe4436952d
parent 57958 045c96e3edf0
child 58957 c9e744ea8a38 
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -385,8 +385,6 @@
     : (Domain_Take_Proofs.iso_info list
        * Domain_Take_Proofs.take_induct_info) * theory =
   let
-    val _ = Theory.requires thy (Context.theory_name @{theory}) "domain isomorphisms"
-
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>
       Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) =>
isabelle