# HG changeset patch
# User clasohm
# Date 826714525 -3600
# Node ID 5a63ab90ee8ab88787b3570bdc0b715a540a479b
# Parent  6d66b59f94a97aa886848be8a2075b9159ab7ca6
modified primrec so it can be used in MiniML/Type.thy

diff -r 6d66b59f94a9 -r 5a63ab90ee8a src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Tue Mar 12 14:39:34 1996 +0100
+++ b/src/HOL/datatype.ML	Wed Mar 13 11:55:25 1996 +0100
@@ -42,9 +42,8 @@
                    \ in recursive application on rhs"
               in 
                 (case assoc (pairs,xk) of 
-                   None => raise RecError 
-                     ("illegal occurence of " ^ fname ^ " on rhs")
-                 | Some(U) => list_comb(U,map subst (ls @ rs)))
+                   None   => list_comb(f, map subst b)
+                 | Some U => list_comb(U, map subst (ls @ rs)))
               end
           else list_comb(f, map subst b)
         end
@@ -393,16 +392,12 @@
              ,list_comb(rec_comb
                         , fns @ map Bound (0 ::(length ls downto 1))));
           val sg = sign_of thy;
-          val defpair =  mk_defpair (Const(fname,dummyT),rhs)
+          val defpair = (fname ^ "_" ^ tname ^ "_def",
+                         Logic.mk_equals (Const(fname,dummyT), rhs))
           val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
           val varT = Type.varifyT T;
           val ftyp = the (Sign.const_type sg fname);
-        in
-          if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
-          then add_defs_i [defpairT] thy
-          else error("Primrec definition error: \ntype of " ^ fname 
-                     ^ " is not instance of type deduced from equations")
-        end;
+        in add_defs_i [defpairT] thy end;
 
     in
       datatypes := map (fn (x,_,_) => x) cons_list' @ (!datatypes);
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);