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/domaindef.ML
changeset 49833 1d80798e8d8a
parent 49759 ecf1d5d87e5e
child 52732 b4da1f2ec73f 
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Fri Oct 12 15:08:29 2012 +0200
@@ -162,12 +162,8 @@
     val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef
     val liftprj_def = singleton (Proof_Context.export lthy ctxt_thy) liftprj_ldef
     val liftdefl_def = singleton (Proof_Context.export lthy ctxt_thy) liftdefl_ldef
-    val type_definition_thm =
-      Raw_Simplifier.rewrite_rule
-        (the_list (#set_def (#2 info)))
-        (#type_definition (#2 info))
     val typedef_thms =
-      [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def,
+      [#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def,
       liftemb_def, liftprj_def, liftdefl_def]
     val thy = lthy
       |> Class.prove_instantiation_instance
isabelle