--- 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);