diff -r 6d66b59f94a9 -r 5a63ab90ee8a src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Tue Mar 12 14:39:34 1996 +0100
+++ b/src/HOL/thy_syntax.ML	Wed Mar 13 11:55:25 1996 +0100
@@ -171,9 +171,13 @@
 
 fun mk_primrec_decl ((fname, tname), axms) =
   let
+    (*Isolate type name from the structure's identifier it may be stored in*)
+    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
+
     fun mk_prove (name, eqn) =
       "val " ^ name ^ " = store_thm (" ^ quote name
-      ^ ", prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
+      ^ ", prove_goalw thy [get_def thy "
+      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
       \  (fn _ => [Simp_tac 1]));";
 
     val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);