# HG changeset patch
# User haftmann
# Date 1155017979 -7200
# Node ID 0bfdbbe657eb2c7f7d332c7c686dd20d7c5173ce
# Parent  d73e49780ef25a75a8243048a18ee27708ac598a
improved & fixed code generator theorem generation

diff -r d73e49780ef2 -r 0bfdbbe657eb src/HOL/Tools/typedef_codegen.ML
--- a/src/HOL/Tools/typedef_codegen.ML	Tue Aug 08 08:19:30 2006 +0200
+++ b/src/HOL/Tools/typedef_codegen.ML	Tue Aug 08 08:19:39 2006 +0200
@@ -112,7 +112,7 @@
             UNIV_I
             |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
             |> rewrite_rule [symmetric def];
-        in case try (Tactic.rule_by_tactic ((ALLGOALS o match_tac) [exists_thm])) inject
+        in case try (op OF) (inject, [exists_thm, exists_thm])
          of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]),
              (ALLGOALS o match_tac) [eq_reflection]
             THEN (ALLGOALS o match_tac) [eq_thm])
@@ -132,7 +132,7 @@
                 UNIV_I
                 |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
                 |> rewrite_rule [symmetric def]
-            in case try (Tactic.rule_by_tactic ((ALLGOALS o match_tac) [exists_thm])) inverse
+            in case try (op OF) (inverse, [exists_thm, exists_thm])
              of SOME eq_thm => SOME [eq_thm]
               | NONE => NONE
             end