author | wenzelm |
Wed, 14 Nov 2001 23:18:37 +0100 | |
changeset 12188 | e4279b7fb8cc |
parent 12187 | a1000fcf636e |
child 12189 | 4729bbf86626 |
--- a/src/ZF/Tools/primrec_package.ML Wed Nov 14 23:18:13 2001 +0100 +++ b/src/ZF/Tools/primrec_package.ML Wed Nov 14 23:18:37 2001 +0100 @@ -176,7 +176,7 @@ val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); val (thy1, [def_thm]) = thy - |> Theory.add_path (Sign.base_name (#1 def)) + |> Theory.add_path (Sign.base_name fname) |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]; val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)