# HG changeset patch
# User wenzelm
# Date 1005776317 -3600
# Node ID e4279b7fb8ccca56780edb087a26f58e5a33fee3
# Parent  a1000fcf636ed4970a12e97918ada5cd72f28113
fix path prefix;

diff -r a1000fcf636e -r e4279b7fb8cc src/ZF/Tools/primrec_package.ML
--- 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)