# HG changeset patch
# User huffman
# Date 1258759796 28800
# Node ID 7f12ab745298d1a985618a5222387b50f625fadd
# Parent  5dac897d91ce0ee5b97873ad8cca33c605a279ed
make repdef work without (open) option

diff -r 5dac897d91ce -r 7f12ab745298 src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Fri Nov 20 14:35:55 2009 -0800
+++ b/src/HOLCF/Tools/repdef.ML	Fri Nov 20 15:29:56 2009 -0800
@@ -121,8 +121,12 @@
     val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy3);
     val [emb_def, prj_def, approx_def] =
       ProofContext.export lthy3 ctxt_thy [emb_ldef, prj_ldef, approx_ldef];
+    val type_definition_thm =
+      MetaSimplifier.rewrite_rule
+        (the_list (#set_def info))
+        (#type_definition info);
     val typedef_thms =
-      [#type_definition info, #below_def cpo_info, emb_def, prj_def, approx_def];
+      [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def];
     val thy4 = lthy3
       |> Class.prove_instantiation_instance
           (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
@@ -130,7 +134,7 @@
 
     (*other theorems*)
     val typedef_thms' = map (Thm.transfer thy4)
-      [#type_definition info, #below_def cpo_info, emb_def, prj_def];
+      [type_definition_thm, #below_def cpo_info, emb_def, prj_def];
     val ([REP_thm], thy5) = thy4
       |> Sign.add_path (Binding.name_of name)
       |> PureThy.add_thms