- Exported functions new_name and new_names
authorberghofe
Fri Dec 10 16:55:58 2004 +0100 (2004-12-10)
changeset 15398055c01162eaa
parent 15397 5260ac75e07c
child 15399 683d83051d6a
- Exported functions new_name and new_names
- Fixed incompatible signatures problem in unfold_attr
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Fri Dec 10 16:54:17 2004 +0100
     1.2 +++ b/src/Pure/codegen.ML	Fri Dec 10 16:55:58 2004 +0100
     1.3 @@ -41,6 +41,8 @@
     1.4    val mk_const_id: Sign.sg -> string -> string
     1.5    val mk_type_id: Sign.sg -> string -> string
     1.6    val rename_term: term -> term
     1.7 +  val new_names: term -> string list -> string list
     1.8 +  val new_name: term -> string -> string
     1.9    val get_defn: theory -> string -> typ -> ((term list * term) * int option) option
    1.10    val is_instance: theory -> typ -> typ -> bool
    1.11    val parens: Pretty.T -> Pretty.T
    1.12 @@ -248,10 +250,7 @@
    1.13        (fst (Logic.dest_equals (prop_of eqn))));
    1.14      fun prep thy = map (fn th =>
    1.15        if name mem term_consts (prop_of th) then
    1.16 -        let val sg = sign_of_thm eqn
    1.17 -        in rewrite_rule [eqn] (if Sign.subsig (sign_of_thm th, sg) then
    1.18 -          Thm.transfer_sg sg th else th)
    1.19 -        end
    1.20 +        rewrite_rule [eqn] (Thm.transfer thy th)
    1.21        else th)
    1.22    in (add_preprocessor prep thy, eqn) end;
    1.23