# HG changeset patch
# User berghofe
# Date 1102694158 -3600
# Node ID 055c01162eaac8ad98b19b4343f4ec83f79e45d3
# Parent  5260ac75e07c55a6c66a8d75644b77cf26a8023f
- Exported functions new_name and new_names
- Fixed incompatible signatures problem in unfold_attr

diff -r 5260ac75e07c -r 055c01162eaa src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Dec 10 16:54:17 2004 +0100
+++ b/src/Pure/codegen.ML	Fri Dec 10 16:55:58 2004 +0100
@@ -41,6 +41,8 @@
   val mk_const_id: Sign.sg -> string -> string
   val mk_type_id: Sign.sg -> string -> string
   val rename_term: term -> term
+  val new_names: term -> string list -> string list
+  val new_name: term -> string -> string
   val get_defn: theory -> string -> typ -> ((term list * term) * int option) option
   val is_instance: theory -> typ -> typ -> bool
   val parens: Pretty.T -> Pretty.T
@@ -248,10 +250,7 @@
       (fst (Logic.dest_equals (prop_of eqn))));
     fun prep thy = map (fn th =>
       if name mem term_consts (prop_of th) then
-        let val sg = sign_of_thm eqn
-        in rewrite_rule [eqn] (if Sign.subsig (sign_of_thm th, sg) then
-          Thm.transfer_sg sg th else th)
-        end
+        rewrite_rule [eqn] (Thm.transfer thy th)
       else th)
   in (add_preprocessor prep thy, eqn) end;