modified primrec so it can be used in MiniML/Type.thy
authorclasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13)
changeset 15745a63ab90ee8a
parent 1573 6d66b59f94a9
child 1575 4118fb066ba9
modified primrec so it can be used in MiniML/Type.thy
src/HOL/datatype.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/datatype.ML	Tue Mar 12 14:39:34 1996 +0100
     1.2 +++ b/src/HOL/datatype.ML	Wed Mar 13 11:55:25 1996 +0100
     1.3 @@ -42,9 +42,8 @@
     1.4                     \ in recursive application on rhs"
     1.5                in 
     1.6                  (case assoc (pairs,xk) of 
     1.7 -                   None => raise RecError 
     1.8 -                     ("illegal occurence of " ^ fname ^ " on rhs")
     1.9 -                 | Some(U) => list_comb(U,map subst (ls @ rs)))
    1.10 +                   None   => list_comb(f, map subst b)
    1.11 +                 | Some U => list_comb(U, map subst (ls @ rs)))
    1.12                end
    1.13            else list_comb(f, map subst b)
    1.14          end
    1.15 @@ -393,16 +392,12 @@
    1.16               ,list_comb(rec_comb
    1.17                          , fns @ map Bound (0 ::(length ls downto 1))));
    1.18            val sg = sign_of thy;
    1.19 -          val defpair =  mk_defpair (Const(fname,dummyT),rhs)
    1.20 +          val defpair = (fname ^ "_" ^ tname ^ "_def",
    1.21 +                         Logic.mk_equals (Const(fname,dummyT), rhs))
    1.22            val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
    1.23            val varT = Type.varifyT T;
    1.24            val ftyp = the (Sign.const_type sg fname);
    1.25 -        in
    1.26 -          if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
    1.27 -          then add_defs_i [defpairT] thy
    1.28 -          else error("Primrec definition error: \ntype of " ^ fname 
    1.29 -                     ^ " is not instance of type deduced from equations")
    1.30 -        end;
    1.31 +        in add_defs_i [defpairT] thy end;
    1.32  
    1.33      in
    1.34        datatypes := map (fn (x,_,_) => x) cons_list' @ (!datatypes);
     2.1 --- a/src/HOL/thy_syntax.ML	Tue Mar 12 14:39:34 1996 +0100
     2.2 +++ b/src/HOL/thy_syntax.ML	Wed Mar 13 11:55:25 1996 +0100
     2.3 @@ -171,9 +171,13 @@
     2.4  
     2.5  fun mk_primrec_decl ((fname, tname), axms) =
     2.6    let
     2.7 +    (*Isolate type name from the structure's identifier it may be stored in*)
     2.8 +    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
     2.9 +
    2.10      fun mk_prove (name, eqn) =
    2.11        "val " ^ name ^ " = store_thm (" ^ quote name
    2.12 -      ^ ", prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
    2.13 +      ^ ", prove_goalw thy [get_def thy "
    2.14 +      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
    2.15        \  (fn _ => [Simp_tac 1]));";
    2.16  
    2.17      val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);